$ 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:
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:
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:
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.
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:
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:
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:
Old (1992). Many article in 199x.
The system is implemented in Common Lisp, and is released under the GNU General Public License (GPL).
See:
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:
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:
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: