Mercurial Mercurial > tips / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
auto-proof.rst
changeset 1911 870693ce6ff0
child 1912 8b81a8f0f692 
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/auto-proof.rst	Mon Feb 22 13:34:55 2016 +0200
@@ -0,0 +1,206 @@
+.. -*- coding: utf-8; -*-
+.. include:: HEADER.rst
+
+================
+ Theorem prover
+================
+.. contents::
+   :local:
+
+Info/links
+==========
+
+ * 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://isarmathlib.org/
+    Home page
+  http://savannah.nongnu.org/projects/isarmathlib
+    Project page
+  http://lists.nongnu.org/mailman/listinfo/isarmathlib-devel
+    Mail list
+
+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)
+
tips