Learning Automated Theorem Proving

cs.stackexchange https://cs.stackexchange.com/questions/820

Question

I am learning Automated Theorem Proving / SMT solvers / Proof Assistants by myself and post a series of questions about the process, starting here.

Note that these topics are not easily digested without a background in (mathematical) logics. If you have problems with basic terms, please read up on those, for instance Logics in Computer Science by M. Huth and M. Ryan (in particular chapters one, two and four) or An Introduction to Mathematical Logic and Type Theory by P. Andrews.
For a short introduction into higher order logic (HOL) see here.

I looked at Coq and read the first chapter of the intoduction to Isabelle amongst others; Types of Automated Theorem Provers

I have known Prolog for a few decades and am now learning F#, so ML, O'Caml and LISP are a bonus. Haskell is a different beast.

I have the following books

"Handbook of Automated Reasoning" edited by Alan Robinson and Andrei Vornkov

"Handbook of Practical Logic and Automated Reasoning" by John Harrison

"Term Rewriting and All That" by Franz Baader and Tobias Nipkow

  1. What are the differences between Coq and Isabelle?

  2. Should I learn either Isabelle or Coq, or both?

  3. Is there an advantage to learning either Isabelle or Coq first?

Find the series' next question here.

Was it helpful?

Solution

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 have a lot of library support and active communities doing all sorts of development and example theories. If one language provides adequate library (or other) support for the kinds of theory you wish to develop, then I'd select that language.

One strategy is to do a simple tutorial in both languages and follow up the one that feels the best. For example,

Here is a blog post briefly comparing the two by someone who ultimately prefers Isabelle.

Make sure you use a proper IDE (such as ProofGeneral), rather than doing things on the command line.

Another way to to get into Coq is to try the online book Software Foundations by Benjamin Pierce et al. It provides an excellent tutorial with loads of details provided. The focus is mostly on programming language semantics, but a lot of the basics (and beyond) of Coq and semi-automated theorem proving are covered along the way.

OTHER TIPS

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 first set out to learn about theorem proving related things, the first book I read (although now quite dated?) was Melvin Fitting's excellent First Order Logic and Automated Theorem Proving. This book was a really excellent one that covered the kinds of topics you'll see that relate to the lower order logics, where you can actually get a fair amount of automation. The kind of logic you learn should be dictated by what you want to reason about, and not so much theorem proving for the sake of it. For example, while first order logic gives you a fair amount of expressiveness and reasoning ability, most of the programming languages community (where I've ended up these days) has departed from the older school of theorem proving and model checking (which go into the bucket of things which are more decidable but less expressive).

Don't take this to mean -- however -- that things like first order reasoning and model checking haven't been extremely useful in practice. They have been! You can look at ACL2 as an example of a prover built atop first order logic which has sen an amazing amount of success in the industrial realm. Along with that, there has also been an amazing amount of development in SMT solving. Modern SMT solvers are built on top of very powerful SAT solvers (mostly through discoveries within the last twenty years for improvements on DPLL), and have seen a great amount of use in things like symbolic execution.

However, as I said, while the more traditional "theorem proving" bit is fun, there's a lot more to learn. Learning Coq -- for example -- has little to do about learning the automation tools it gives you, and has a lot more to do with learning the type theory upon which it's based (the predicative calculus of coinductive constructions). If you're not used to constructive logic, the curry howard isomorphism, or type theory, you'll have an exciting time learning these tools, but I can hardly think that they're too closely related to things you see in the first volume of the handbook.

So decide what you want to do: verify models and theorems in first order logic, or use a powerful type theory to reason about correctness of your programs (or theorems in constructive logic). If it's the first, learn about more automated deduction based techniques, if it's the second, learn more about Coq, HOL, etc... By the way, if you want to learn Coq, while the above references are good, I think that there are two really core references for learning Coq:

Benjamin Pierce's software foundations book (Dr. Pierce is an excellent writer, and I'd recommend you also look at his more popular "brick book," if you haven't yet).

Certified Programming with Dependent Types (Adam Chlipala also writes quite well, though his books assume a bit more maturity and intelligence than Pierce's perhaps simpler introduction.)

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, Italian, Spanish, Portuguese. All of them are somehow related -- this is not Chinese -- but very few people manage all of that simultaneously. So you should try get a taste for each of the cultures and communities, and then make a commitment.

There might be also the "killer feature" that you really need for your work.

It also helps to have fellow experts on one of these systems around.

  • What are the differences between Coq and Isabelle?

Both are descendants of the LCF system from Stanford/Edinburgh/Cambridge. In 1985, G. Huet and L. Paulson were working together on the last version of Cambridge LCF. Then the split happened towards Coc/CIC/COQ (now Coq) in France, and Isabelle in Cambridge and Munich. Note that HOL4, HOL-Light, HOL-XYZ are other related descendants of LCF.

More than 20 years ago, the distinction of Coq vs. Isabelle would have been made according to logical foundations: Dependently Typed Constructive Logic here, Simpl-Typed Classical Logic there. Today, there is surprisingly little impact on that in practice, since more and more layers have been added on top of each formal system, including add-on tools, and libraries.

  • Should I learn either Isabelle or Coq, or both?

You should look at both, and try to get a feeling if you like more Wine and Cheese, or Bratwurst and Sauerkraut. (As one of the guys behind Isabelle, but presently at France, I am surprised how many Frenchmen actually like Sauerkraut when they are privately at home and nobody looking :-)

  • Is there an advantage to learning either Isabelle or Coq first?

I don't think so. There might be a danger that you get stuck with the one you try first and don't try the second, or that you get disappointed too early with the first and dismiss it too early. In any case, you will need time and persistence to become productive with either system.

Since Proof General as "IDE" was mentioned already: Proof General / Emacs used to be the standard unifying interface for both Coq and Isabelle over many years, but I would never have called it an IDE. There is also CoqIDE with "IDE" in its name, but is a relatively basic editor on top of Gtk widgets. Current Isabelle includes Isabelle/jEdit, which does not have "IDE" in its name, but is meant to approximate things you see routinely in Netbeans or IntelliJ IDEA --- for proof texts instead of Java code.

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

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

I've recently came to these Coq tutorials from $\lambda$conf2017 so I've figured out it's worth sharing here for whoever visits this question later.

Also, DeepSpec Summer School's Software Foundations has some pretty cool lectures:

Some of the lectures based on the Software foundations series, that was already mentioned.

Licensed under: CC-BY-SA with attribution
Not affiliated with cs.stackexchange
scroll top