41

I recommend reading Pollack's How to believe a machine-checked proof. It explains how proof assistants are designed to minimize the amount of critical code. There are many levels of formal verification (that's the phrase you're looking for in place of "proven") of a proof assistant: Verify that the algorithms used by the proof assistant are correct. Verify ...


20

Most of your statements are elementary algebra, so these can be proved automatically by a computer algebra system (CAS), such as Maple or Mathematica. (In case you're interested in the mathematics behind CAS, I can recommend the book Modern Computer Algebra by Joachim von zur Gathen and Jürgen Gerhard, a beautiful book, considered the 'bible' of the field) ...


15

There is a variety of systems for Interactive Theorem Proving (ITP) -- see also the conference of that name -- Coq, Isabelle, HOLs, ACL2, PVS etc. All of them are relatively challenging to learn, and each has its own specific culture. It is like learning a foreign language: lets say you know English already, and then have the choice of French, German, ...


11

We have to be carful here. I think you mean that a program given a formula could not, in general, produce a proof of it or its negation. I can write a program that, given a theorem, will produce it's proof as long as the set of proofs is recursively enumerable. This is not possible in general because of Godel's incompleteness theorem (well that was the first ...


11

What is second order logic in contrast to first order logic? What is monadic vs non monadic logic? Monadic second-order logic is first-order logic plus quantification over sets. So, as well as being able to say that there exists a domain element with some property ($\exists x\dots$), you can also say that there exists a set of domain elements with some ...


10

I don't know why people didn't develop Hoare logics for lambda-calculi earlier. The first work to get this right was Honda et al's A Compositional Program Logic for Polymorphic Higher-Order Functions There were some earlier attempts before this, but they didn't quite nail the problem, for example: how do you denote the value of a functional program? What ...


10

There are many related ways you can mechanise your logic. Deep embedding into one of the well-developed provers such as Isabelle/HOL, Coq or Agda. This is (almost) always possible, but makes using the embedded logic awkward. Shallow embedding into one of the well-developed provers such as Isabelle/HOL, Coq or Agda. This is only possible when the embedded ...


9

A little google-fu (and my own memory) tells me it was apparently named by Larry Paulson after Gerard Huet's daughter. Gerard Huet happens to be one of the people behind the less poetically named Coq theorem prover. Small world!


9

What you need is the idea of "the trusted core". Quoting "A verified runtime for a verified theorem prover": In many theorem provers, the trusted core—the code that must be right to ensure faithfulness—is quite small. As examples, HOL Light is an LCF-style system whose trusted core is 400 lines of Objective Caml, and Milawa is a Boyer-Moore style prover ...


8

To simplify a bit, a system of inference rules generally defines a set of sequents, which are simply pairs of a list (or set) of propositions $\Gamma$ and a proposition $\phi$ written $$ \Gamma \vdash \varphi$$ called the derivable sequents. The rules describe which sequents are derivable, and for any reasonable system, given $\Gamma\vdash\varphi$, and ...


8

The existential form of the axioms of set theory is convenient for the meta-theoretic explorations of set theory, such as forcing etc., where it is important to have a minimal language to worry about (only $\in$ relation). But even just stating the axioms of set theory without any constants and operation symbols is pretty haunting, see this gist of mine. If ...


7

I would say that the classic distinction of "automated theorem proving" (ATP) vs. "interactive theorem proving" (ITP) needs to be reconsidered. If you take a well-known ITP system like Isabelle/HOL today (Isabelle2013 from February 2013), it integrates quite a lot of add-on tools from the ATP portfolio: On-board generic automated proof tools: old-school ...


7

Coq is a bit more cruel than paper proofs: when you write "and we are done" or "clearly" in a paper proof, there is often much more to do to convince Coq. Now I did a little clean up of your code, while trying to keep it in the same spirit. You can find it here. Several remarks: I used built in datatypes and definitions where I thought it wouldn't hurt ...


6

Edit: I found a better example. Consider these clauses: \begin{align} & \lnot P(x) \lor P(f(x)) \\ & P(x) \\ & \lnot P(f(f(x)))\\ \end{align} Obviously, this set of clauses is contradictory. But without renaming variables, the only possible resolvent is $P(f(x))$ and no more resolvents are possible - all lead to substituting $f(x)$ for $x$, which ...


6

While this may trend close to self-advertisement, this is essentially the topic of my recent paper Metamath Zero: The Cartesian Theorem Prover (video), and the analogy with bootstrapping compilers is spot on. The introduction of the paper lays out what is needed to make this happen, and it's only a problem of engineering. As Andrej says, there are several ...


5

How would you prove inside the pure CoC that the induction principle holds of the Church numerals? See Thomas Streicher's, Independence of the induction principle and the axiom of choice in the pure calculus of constructions.


5

Yes, there is a generalization of the construction you mentioned. However, it's utility depends on the function F. The guarantees you get are meaningful only if F is robust, in the sense that you have to change a large fraction of the dataset to make any (meaningful) change to the output of the computation. Suppose we have an untrusted agent Agatha who is ...


5

Use a model checker. This is exactly what they're good for. You might look at SPIN and NuSMV as a starting point, but there are many others as well.


5

This is late for you, but probably might be of help to others. I myself had asked this question and I wrote the summary of my findings to the acl2-help mailing list on 8 and 9 September 2013: https://utlists.utexas.edu/sympa/arc/acl2-help/2013-09/msg00005.html https://utlists.utexas.edu/sympa/arc/acl2-help/2013-09/msg00006.html Disclaimer: What follows is ...


5

Inductive creates a new type and gives it a name. It is similar to datatype in SML, data in Haskell, type (defining an ordinary variant or a record) in Ocaml. In addition to defining the type, Inductive also defines induction principles for that type. These induction principles aren't necessary from a theoretical point of view: all they do is to give a name ...


4

This introduction to Isabelle is pretty exhaustive. Also see this introduction to Isabelle In general, Isabelle is relatively easy to start with, as there are many available examples. For example, in the official website P.S - I am in no way affiliated with Isabelle, I'm a theoretician in formal methods, but I know Isabelle comes up often as a default ...


4

If you indeed follow the construction in the way you describe, then there might be states which are unreachable from the starting state. That's allowed in a DFA, though you can go ahead and remove them without affecting the operation of the automaton.


4

It is true that this construction may result in a DFA with unreachable states. The general construction begins simply by including all possible states, then adding the appropriate transitions, so typically the resulting DFA won't be the smallest DFA that accepts the same language (in terms of the number of states). An alternative approach is to only add ...


4

If you believe that a proof or disproof has reasonable length, you could come up with one SAT instance which states $x_1,\ldots,x_n$ encodes a proof of the Riemann Hypothesis, and another one stating $x_1,\ldots,x_n$ encodes a refutation of the Riemann hypothesis. The formula will have size polynomial in $n$, though probably not linear; if you're careful, ...


4

Cody's answer is excellent, and fulfils your question about translating your proof to Coq. As a complement to that, I wanted to add the same results, but proven using a different route, mainly as an illustration of some bits of Coq and to demonstrate what you can prove syntactically with very little additional work. This is not a claim however that this is ...


4

Essentially, you can treat uninterpreted predicates as boolean-valued functions (adding a new boolean sort if necessary) and replace them with boolean variables as you would other functions. For the given example: Getting rid of $F$ and $G$ first: $$\begin{align*} p(z,f_1)&\wedge f_2=g_1\to p(x_1,y)\wedge x_1=f_1\to f_1=f_2\\ &\wedge x_1=x_2\to ...


4

This is certainly possible, and the language of higher order functions makes this quite nice. If you're doing a Turing/Cook reduction, you can basically just write a function that takes an oracle as a parameter. For example, to show that Graph Coloring is NP-hard, you could write something like this (pardon my terrible Coq-like pseudocode) Theorem ...


3

All of the theorems you want to prove (except uniqueAddNeutral) are of the form $\forall x . \phi(x)$ where $\phi(x)$ is quantifier-free. Herbrandization is typically the first step towards proving those theorems: replace $x$ with an arbitrary constant $c$, with no assumptions made about $x$, and prove $\phi(c)$ holds without making any assumptions about $c$...


3

(Note: I don't know anything about geometric reasoning, so I'm shifting from my limited experience in automated theorem proving in another field. I think the fundamental issue is the same.) Synthetic reasoning tends to blow up exponentially. Typically, after $n$ steps of reasoning, there are about $a^k$ ways to choose a next step for some $a \gt 1$. There ...


3

This is a project I've been thinking of venturing into for a few years now, and I was fortunate to have a very useful discussion about it at the time I started planning it with Chris Lattner (at the time, one of the main architects of LLVM, although better known these days perhaps for his work on Swift). It does seem that there is a possibility of producing ...


Only top voted, non community-wiki answers of a minimum length are eligible