16
$\begingroup$

Is there any web-based course or materials about logic / automatic theorem proving? (I checked MIT's OpenCourseWare and I only found a vaguely related AI course)

Improve this question
$\endgroup$

7 Answers 7

Reset to default
8
$\begingroup$

There are basically two historical veins of automated theorem proving, either you accept a weakened logic in exchange for more automation eg ACL2, or you accept some fairly weak automation in exchange for a strong logic . Fortunately, there are some relatively modern tools such as Coq (and I suppose Isabelle/HOL) which support both veins of theorem proving.

If you want a short concrete taste of this, I'd suggest checking out this tutorial by adam chipala which exposits some techniques in Coq that are very clever which allow for easy reasoning in at least the context of programming language theory. That aside, all these websites have a number of good references for good tutorials both about proof assistants and how to use them.

Improve this answer
$\endgroup$
2
  • $\begingroup$ just out of curiosity, how is adam.chlipala.net/cpdt a tutorial? It seems to be an entire book! How did you specifically had in mind to go through it? $\endgroup$
    – Charlie Parker
    Commented Nov 3, 2017 at 22:47
  • 2
    $\begingroup$ it wasn't a book at first :) . Notice how it was first published as a book in 2013, 4-5 years after i linked it :) $\endgroup$
    – Carter Tazio Schonwald
    Commented Nov 28, 2017 at 20:07
4
$\begingroup$

I'll repeat the suggestion and highly recommend Frank Pfenning's course notes, which you can also find at the original course website (google "15-815 cmu"). Another book you can try is Jean Gallier's Logic for Computer Science: Foundations of Automatic Theorem Proving, recently recommended on a LambdaTheUltimate thread.

Improve this answer
$\endgroup$
4
$\begingroup$

John Harrison "Handbook of Practical Logic and Automated Reasoning" - superbook

Improve this answer
$\endgroup$
2
$\begingroup$

Materials for one course on Isabelle (previously mentioned) are available.

Improve this answer
$\endgroup$
1
$\begingroup$

I haven't read any of these but they might be useful:

Some notes of Frank Pfenning.

A paper of Wirth.

Improve this answer
$\endgroup$
1
$\begingroup$

Benjamin Pierce has a nice introduction to automatic theorem proving in his Software Foundations Courseware, using Coq.

Improve this answer
$\endgroup$
1
$\begingroup$

Have you heard of the Coq proof assistant? It is quite popular here in France. The official webpage contains good documetation.

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .