1.1.1 General links

Here are some links on mathematical and automated theorem proving.

• Wiki. Atp.
• See the QEDEQ system for mathematical theorem proving.
• Mathematical theorem proving via Hilbert’s program is claimed to be impossible to solve due to the Godel incompleteness theorem. Even though it is considered to be impossible, people are still working on the Hilbert program and on variations of it. It would be amazing to prove the Godel incompleteness theorem to be false. Some people think this could happen any time.
• TPTP library of test programs.
• Discussion with references.
• Xah Lee. See his live blog discussion of some aspects in this area. Also see his codification discussion and the many references contained therein.
• SASyLF. Automated proof using the Scala programming language.
• MSDN Blog on theorem provers.
• Verify all theorems on boot! This blog article by Frank Hecker contains many useful references. This review paper lists feats from other theorem provers.
• The HOL Light theorem prover.
  • Flyspeck project. Kepler conjecture.
  • List of theorems that have been proved with HOL light. This is amazing! It is also amazing to see how theorems are expressed in terms of this language.
• Interactive proof assistant called Coq.
• Open theory attempts to allow the different theorem provers to communicate. A pdf slide show provides a nice summary.
• jImp theorem prover.
• On-line course. Another course is found here.
  • pdf for course by Frank Pfenning at CMU, handouts.
• Some citations.
• Logic with Prolog.
• Some notes on ACL2. Acl2.
• Automated math development book review.

This document was generated by George Schils on June 16, 2010 using texi2html 1.82.

Copyright © 2010 George Schils. All rights reserved.