most recent 30 from http://mathoverflow.net 2013-05-21T08:38:49Z http://mathoverflow.net/feeds/question/1017 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/1017/intro-to-automatic-theorem-proving-logical-foundations unknown (google) 2009-10-18T08:52:21Z 2010-02-18T13:54:31Z

<p>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)</p>

http://mathoverflow.net/questions/1017/intro-to-automatic-theorem-proving-logical-foundations/1029#1029 Andreas Holmstrom 2009-10-18T12:48:36Z 2009-10-18T12:48:36Z

<p>I haven't read any of these but they might be useful:</p> <p>Some <a href="http://www.cs.mcgill.ca/~bpientka/courses/comp527/handouts/atp.pdf" rel="nofollow">notes of Frank Pfenning</a>.</p> <p>A <a href="http://front.math.ucdavis.edu/0902.3294" rel="nofollow">paper of Wirth</a>.</p>

http://mathoverflow.net/questions/1017/intro-to-automatic-theorem-proving-logical-foundations/1052#1052 Carter Tazio Schonwald 2009-10-18T17:27:03Z 2009-10-18T17:27:03Z

<p>There are basically two historical veins of automated theorem proving, either you accept a weakened logic in exchange for more automation eg <a href="http://www.cs.utexas.edu/users/moore/acl2/" rel="nofollow">ACL2</a>, or you accept some fairly weak automation in exchange for a strong logic . Fortunately, there are some relatively modern tools such as <a href="http://coq.inria.fr/" rel="nofollow">Coq</a> (and I suppose <a href="http://www.cl.cam.ac.uk/research/hvg/Isabelle/" rel="nofollow">Isabelle/HOL</a>) which support both veins of theorem proving. </p> <p>If you want a short concrete taste of this, I'd suggest checking out <a href="http://adam.chlipala.net/cpdt/" rel="nofollow">this</a> 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.</p>

http://mathoverflow.net/questions/1017/intro-to-automatic-theorem-proving-logical-foundations/1301#1301 Jay Kominek 2009-10-19T22:17:03Z 2009-10-19T22:17:03Z

<p>Materials for one course on Isabelle (previously mentioned) <a href="http://www.cs.colorado.edu/~siek/7000/spring07/" rel="nofollow">are available</a>.</p>

http://mathoverflow.net/questions/1017/intro-to-automatic-theorem-proving-logical-foundations/1521#1521 1331 2009-10-20T23:25:23Z 2009-10-20T23:25:23Z

<p>Benjamin Pierce has a nice introduction to automatic theorem proving in his <a href="http://www.cis.upenn.edu/~bcpierce/sf/toc.html" rel="nofollow">Software Foundations Courseware</a>, using Coq.</p>

http://mathoverflow.net/questions/1017/intro-to-automatic-theorem-proving-logical-foundations/1989#1989 Noam Zeilberger 2009-10-23T00:25:24Z 2009-10-23T00:25:24Z

<p>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 <a href="http://www.cis.upenn.edu/~jean/gbooks/logic.html" rel="nofollow">Logic for Computer Science: Foundations of Automatic Theorem Proving</a>, recently recommended on a LambdaTheUltimate thread.</p>

http://mathoverflow.net/questions/1017/intro-to-automatic-theorem-proving-logical-foundations/2074#2074 subshift 2009-10-23T11:34:35Z 2009-10-23T11:34:35Z

<p>Have you heard of the <a href="http://coq.inria.fr/" rel="nofollow">Coq proof assistant</a>? It is quite popular here in France. The official webpage contains good <a href="http://coq.inria.fr/documentation" rel="nofollow">documetation</a>.</p>

http://mathoverflow.net/questions/1017/intro-to-automatic-theorem-proving-logical-foundations/2261#2261 boris 2009-10-24T08:15:20Z 2009-10-24T08:15:20Z

<p>John Harrison "Handbook of Practical Logic and Automated Reasoning" - superbook</p>