Decision procedures

Otter 3.3/Mace 2.2 by William McCune — last modified 2007-01-31 15:20

Otter is a resolution-style theorem-proving program for first-order logic with equality. Otter includes the inference rules binary resolution, hyperresolution, UR-resolution, and binary paramodulation. Some of its other abilities and features are conversion from first-order formulas to clauses, forward and back subsumption, factoring, weighting, answer literals, term ordering, forward and back demodulation, evaluable functions and predicates, Knuth-Bendix completion, and the hints strategy. Mace2 is a program that searches for finite models of first-order statements. The statement to be modeled is first translated to clauses, then to relational clauses; finally for the given domain size, the ground instances are constructed. A Davis-Putnam-Loveland- Logeman procedure decides the propositional problem, and any models found are translated to first-order models. Mace2 is a useful complement to the theorem prover Otter, with Otter searching for proofs and Mace2 looking for countermodels. Otter and Mace2 are coded in ANSI C, are free, and are portable to many different kinds of computer.

Simplify Prover Benchmarks by shankar — last modified 2007-01-31 15:37

This directory contains two test suites for automatic theoreom provers. The first test suite, in the subdirectory front_end_suite, consists of 207 files containing 2331 valid verification conditions. The second test suite, in the subdirectory small_suite, consists of 18 files each containing a single valid conjecture. The format of these files is described in the file format.txt.

GAMMA 1 by shankar — last modified 2007-01-31 18:02

J. A. Robinson's historical technical report on a Fortran program implemented for the IBM 704 using instantiation and the Davis-Putnam algorithm for propositional satisfiability.

Mathematical Procedures for Decision Problems by shankar — last modified 2007-01-31 18:07

The original report on Martin Davis' implementation of the Presburger algorithm for the Institute for Advanced Study computer. This is the first theorem prover to be implemented on an electronic computer.

SMT-COMP by Leonardo de Moura — last modified 2005-12-01 17:31

The Satisfiability Modulo Theories Competition

SMT-LIB benchmarks by Leonardo de Moura — last modified 2005-12-02 11:25

SMT benchmarks used in SMT-COMP'05.

Yices by Leonardo de Moura — last modified 2005-12-03 10:26

Decision procedure

ICS by Leonardo de Moura — last modified 2005-12-02 11:32

Decision procedure

SAL decision procedures by Leonardo de Moura — last modified 2006-01-12 14:50

SAL uses ICS.