Welcome to MathOverflow

Question

11

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)

edited Feb 18 2010 at 13:54

Charles Stewart
1,669●8●15

asked Oct 18 2009 at 8:52

unknown (google)
111●3

Andreas Holmstrom · Answer 1 · 2009-10-18 12:48:36Z UTC

1

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

Some notes of Frank Pfenning.

A paper of Wirth.

answered Oct 18 2009 at 12:48

Andreas Holmstrom
2,825●1●12●28

Carter Tazio Schonwald · Answer 2 · 2009-10-18 17:27:03Z UTC

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.

Jay Kominek · Answer 3 · 2009-10-19 22:17:03Z UTC

2

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

answered Oct 19 2009 at 22:17

Jay Kominek
41●3

1331 · Answer 4 · 2009-10-20 23:25:23Z UTC

1

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

answered Oct 20 2009 at 23:25

1331
11●1

Noam Zeilberger · Answer 5 · 2009-10-23 00:25:24Z UTC

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.

subshift · Answer 6 · 2009-10-23 11:34:35Z UTC

1

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

answered Oct 23 2009 at 11:34

subshift
500●4●10

boris · Answer 7 · 2009-10-24 08:15:20Z UTC

3

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

answered Oct 24 2009 at 8:15

boris
31●1

Intro to automatic theorem proving / logical foundations?

Remember to vote up questions/answers you find interesting or helpful (requires 15 reputation points)

7 Answers

You can accept an answer to one of your own questions by clicking the check mark next to it. This awards 15 reputation points to the person who answered and 2 reputation points to you.