Learning Automated Theorem Proving

Answered By : Dave Clarke

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,

• Coq in a Hurry by Yves Bertot, or
• the first part of A Proof Assistant for Higher-Order Logic by Tobias Nipkow, Lawrence C. Paulson and Markus Wenzel.

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.

Problem Detail: 

^{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.}

Asked By : Guy Coder

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/820