# Category/Mathematics/proof-checker

**Broaden your selection:** Category/Mathematics

## Category/Mathematics

*proof-checker* (7)

- Aris
- A sequential proof program, designed to assist anyone interested in solving logical proofs. Aris supports both propositional and predicate logic, as well as Boolean algebra and arithmetical logic in the form of abstract sequences. It uses a predefined set of both inference and equivalence rules, however gives the user options to use older proofs as lemmas, including Isabelle's Isar proofs.

- Coq
- A proof done with Coq is mechanically checked by the machine. In particular, Coq allows:
- to define functions or predicates,
- to state mathematical theorems and software specifications,
- to develop interactively formal proofs of these theorems,
- to check these proofs by a relatively small certification "kernel".

- Metamath
- Metamath is a language and a proof verifier for developing and verifying strictly formalized mathematical proofs, bundled with collaborated databases containing thousands of proven theorems including conventional results in logic, set theory, number theory, group theory, algebra, analysis, topology and various other topics. All proofs are in the form of Hilbert-style formulas.
Included databases:
- ZFC set theory
- New Foundations set theory
- Higher-order logic
- Intuitionistic logic
- Hilbert space
- Quantum logic

- Otter Mace
- Otter is an automated theorem prover for first-order and equational logic, and Mace2 searches for finite models and counterexamples. Otter/Mace2 are no longer being actively developed, and maintenance and support minimal. We recommend using Otter/Mace2's successor Prover9/Mace4 instead.

- Poly ML
- Poly/ML is an extremely fast and efficient implementation of Standard ML and provides several additional features. There is a foreign language interface which allows dynamically linked libraries to be loaded and functions within them called from ML. An X-Windows interface using Motif is available and a symbolic debugger for Poly/ML.

- Prover 9
- Prover9 is an automated theorem prover for first-order and equational logic, and Mace4 searches for finite models and counterexamples. Prover9 is the successor of the Otter prover.

- Zenon
- Zenon is an Extensible Automated Theorem Prover Producing Checkable Proofs Zenon is an automated theorem prover for first order classical logic (with equality), based on the tableau method. Zenon is intended to be the dedicated prover of the Focal environment, an object-oriented algebraic specification and proof system, which is able to produce OCaml code for execution and Coq code for certification.

Permission is granted to copy, distribute and/or modify this document under the terms of the GNU Free Documentation License, Version 1.3 or any later version published by the Free Software Foundation; with no Invariant Sections, no Front-Cover Texts, and no Back-Cover Texts. A copy of the license is included in the page “GNU Free Documentation License”.

The copyright and license notices on this page only apply to the text on this page. Any software or copyright-licenses or other similar notices described in this text has its own copyright notice and license, which can usually be found in the distribution or license text itself.