Episode #125 of the Stack Overflow podcast is here. We talk Tilde Club and mechanical keyboards. Listen now
25

My preference is for Coq, but I imagine that others prefer Isabelle. One of the strange things I found about Isabelle is that there is a two-level syntax, where some of your definitions need to be inside double quote. No such nonsense is present in Coq. Ultimately, the one that is most suitable for you may depend on what you want to prove. Both languages ...


18

One thing that I think you'll find interesting is that the "theorem proving" term varies vastly depending on what field you're in. While they are -- in the abstract -- somewhat related, practical theorem proving (like the kind you see elaborated on in the Handbook of Automated Reasoning) has less to do with Coq or Isabelle than you would think. When I ...


18

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, ...


15

The categorization in that list is certainly still current. Perhaps one new category has emerged, namely, dependently-typed programming languages. These are essentially automated theorem provers where the primary goal is not proving theorems, but programming. Due to the Curry-Howard correspondence, these two concepts are strongly intertwined. The ultimate ...


14

Validity of higher order formulae is in general not decidable and search spaces are huge, so all you can hope to do is to try to find a proof -- assuming it exists -- by cleverly enumerating the proof space (think sledgehammer, aptly named) but that is rough. Humans can play the oracle, providing the key lemmata to guide proof. Automated provers, on the ...


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

Unification is such a fundamental concept in computer science that perhaps at time we even take it for granted. Any time we have a rule or equation or pattern and want to apply it to some data, unification is used to specialize the rule to the data. Or if we want to combine two general but overlapping rules, unification provides us with the most general ...


10

Here are some nice video Coq tutorials by Andrej Bauer. It's in no way complete, but I think it's a good introduction.


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

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 ...


9

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 ...


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

Proof assistants such as Isabelle/HOL work on a syntactical level on a logical calculus. Imagine you have the modus ponens rule (MP) $\qquad \displaystyle P\to Q, P\ \Longrightarrow\ Q$ and the proof goal $\qquad \displaystyle (a \lor b) \to (c \land d), a \lor b \ \overset{!}{\Longrightarrow} c\land d$ We humans see immediately that this follows with ...


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 ...


6

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 ...


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

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 ...


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

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

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

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

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

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

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 ...


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