+
−-*- mode: outline; coding: utf-8; -*-
+
−
+
−* Info/links.
+
−
+
−See
+
−
+
−  http://en.wikipedia.org/wiki/Automated_theorem_proving
+
−
+
−
+
−* proofgeneral.
+
−
+
−  $ sudo apt-get install proofgeneral
+
−  $ sudo apt-get install proofgeneral-coq
+
−  $ sudo apt-get install proofgeneral-misc
+
−  $ sudo apt-get install proofgeneral-doc
+
−  $ sudo apt-get install proofgeneral-minlog
+
−
+
−or build from source:
+
−
+
−  $ make clean
+
−  $ make compile EMACS=xemacs
+
−  $ cat ~/.emacs
+
−...
+
−(load-file "dir/generic/proof-site.el")
+
−...
+
−
+
−See
+
−
+
−  http://proofgeneral.inf.ed.ac.uk/
+
−
+
−* Isabelle.
+
−
+
−Isabelle is a generic proof assistant.
+
−
+
−It allows mathematical formulas to be expressed in a formal language and
+
−provides tools for proving those formulas in a logical calculus. The main
+
−application is the formalization of mathematical proofs and in particular
+
−formal verification, which includes proving the correctness of computer
+
−hardware or software and proving properties of computer languages and
+
−protocols.
+
−
+
−See
+
−
+
−  http://isabelle.in.tum.de/overview.html
+
−  http://en.wikipedia.org/wiki/Isabelle_(theorem_prover)
+
−
+
−* IsarMathLib.
+
−
+
−The goal of the project is to create a library of formalized mathematics,
+
−similar to the Mizar Mathematical Library, but written for the Isabelle/Isar
+
−theorem prover (ZF logic).
+
−
+
−See
+
−
+
−  http://savannah.nongnu.org/projects/isarmathlib
+
−  http://lists.nongnu.org/mailman/listinfo/isarmathlib-devel
+
−
+
−** http://isarmathlib.org/
+
−
+
−This site is an experimental HTML rendering of fragments of the IsarMathLib
+
−project. IsarMathLib is a library of mathematical proofs formally verified by
+
−the Isabelle theorem proving environment. The formalization is based on the
+
−Zermelo-Fraenkel set theory.
+
−
+
−** Tiddly Formal Math.
+
−
+
−This site is an experimental TiddlyWiki rendering of fragments of the
+
−IsarMathLib project. IsarMathLib is a library of mathematical proofs formally
+
−verified by the Isabelle theorem proving environment. The formalization is
+
−based on the Zermelo-Fraenkel set theory.
+
−
+
−See
+
−
+
−  http://formalmath.tiddlyspot.com/
+
−
+
−* HOL Light.
+
−
+
−HOL Light is a computer program to help users prove interesting mathematical
+
−theorems completely formally in higher order logic. It sets a very exacting
+
−standard of correctness, but provides a number of automated tools and
+
−pre-proved mathematical theorems (e.g. about arithmetic, basic set theory and
+
−real analysis) to save the user work. It is also fully programmable, so users
+
−can extend it with new theorems and inference rules without compromising its
+
−soundness.
+
−
+
−Ocalm.
+
−
+
−See
+
−
+
−  http://www.cl.cam.ac.uk/~jrh13/hol-light/index.html
+
−
+
−* ACL2.
+
−
+
−ACL2 (A Computational Logic for Applicative Common Lisp) is a software system
+
−consisting of a programming language, an extensible theory in a first-order
+
−logic, and a mechanical theorem prover. ACL2 is designed to support automated
+
−reasoning in inductive logical theories, mostly for the purpose of software
+
−and hardware verification. The input language and implementation of ACL2 are
+
−built on Common Lisp. ACL2 is free, open source (GPL) software.
+
−
+
−  $ sudo apt-get install acl2
+
−
+
−See
+
−
+
−  http://www.cs.utexas.edu/users/moore/acl2/
+
−  http://en.wikipedia.org/wiki/ACL2
+
−
+
−* PVS Specification and Verification System
+
−
+
−Old (1992). Many article in 199x.
+
−
+
−The system is implemented in Common Lisp, and is released under the GNU
+
−General Public License (GPL).
+
−
+
−See
+
−
+
−  http://pvs.csl.sri.com/
+
−  http://en.wikipedia.org/wiki/Prototype_Verification_System
+
−  http://www-formal.stanford.edu/clt/ARS/Entries/pvs
+
−
+
−* The TPTP Problem Library for Automated Theorem Proving.
+
−
+
−The TPTP (Thousands of Problems for Theorem Provers) is a library of test
+
−problems for automated theorem proving (ATP) systems. The TPTP supplies the
+
−ATP community with:
+
−
+
− * A comprehensive library of the ATP test problems that are available today,
+
−   in order to provide an overview and a simple, unambiguous reference
+
−   mechanism.
+
− * A comprehensive list of references and other interesting information for
+
−   each problem.
+
− * Arbitrary size instances of generic problems (e.g., the N-queens problem).
+
− * A utility to convert the problems to existing ATP systems' formats.
+
− * General guidelines outlining the requirements for ATP system evaluation.
+
− * Standards for input and output for ATP systems.
+
−
+
−The principal motivation for the TPTP is to support the testing and evaluation
+
−of ATP systems, to help ensure that performance results accurately reflect the
+
−capabilities of the ATP system being considered. A common library of problems
+
−is necessary for meaningful system evaluations, meaningful system comparisons,
+
−repeatability of testing, and the production of statistically significant
+
−results. The TPTP is such a library.
+
−
+
−See
+
−
+
−  http://www.cs.miami.edu/~tptp/
+
−
+
−* SPASS.
+
−
+
−An Automated Theorem Prover for First-Order Logic with Equality.
+
−
+
−See
+
−
+
−  http://www.spass-prover.org/index.html
+
−
+
−* Competition.
+
−
+
−See
+
−
+
−  http://www.cs.miami.edu/~tptp/CASC/
+
−  http://www.cs.albany.edu/~nvm/cade.html
+
−
+
−* Conference.
+
−
+
−IJCAR is a series of conferences on the topics of automated reasoning,
+
−automated deduction, and related fields. It is organized semi-regularly as a
+
−merger of other meetings. IJCAR replaces those independent conferences in the
+
−years it takes place. The conference is organized by CADE Inc., and CADE has
+
−always been one of the conferences partaking in IJCAR.
+
−
+
−See
+
−
+
−  http://www.ijcar.org/
+
−  http://en.wikipedia.org/wiki/International_Joint_Conference_on_Automated_Reasoning
+
−
+
−* Top 100.
+
−
+
−  http://www.cs.ru.nl/~freek/100/
+
−                (winner)
+
−  http://personal.stevens.edu/~nkahl/Top100Theorems.html
+
−                (orig list)
+
−  http://www.cse.unsw.edu.au/~kleing/top100/#5
+
−                (Isabelle)