.. -*- coding: utf-8; -*-

================

 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)