Downloads

Forums by admin — last modified 2006-12-07 16:10

This folder contains message boards for multi-way discussion of specific topics of short-term or long-term interest.

PTTP by Mark Stickel — last modified 2007-01-31 15:11

PTTP is a theorem-prover for the first-order predicate calculus that uses the model elimination inference procedure and iterative deepening search. Input formulas are compiled by PTTP for direct execution by Prolog, so individual inference operations are fast.

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.

Murphi 3.1 by David L. Dill — last modified 2007-01-31 15:33

Murphi is a formal verifier based on explicit state enumeration. The verifier performs depth- or breadth-first search in the state graph defined by a Murphi description, storing all the states it encounters in a large hash table.

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.

ACL2 3.0 by shankar — last modified 2007-01-31 15:50

ACL2 (A Computational Logic for Applicative Common Lisp) is a programming language for modeling computer systems and a tool for proving properties of those models. It was developed at the University of Texas at Austin.

HOL 4 by shankar — last modified 2007-01-31 15:54

HOL 4 is the latest version of the HOL automated proof system for higher order logic: a programming environment in which theorems can be proved and proof tools implemented. Built-in decision procedures and theorem provers can automatically establish many simple theorems. An oracle mechanism gives access to external programs such as SAT and BDD engines. HOL 4 is particularly suitable as a platform for implementing combinations of deduction, execution and property checking.

SPIN 4.2.8 by shankar — last modified 2007-01-31 16:01

Spin is a popular open-source software tool, used by thousands of people worldwide, that can be used for the formal verification of distributed software systems. The tool was developed at Bell Labs in the original Unix group of the Computing Sciences Research Center, starting in 1980. The software has been available freely since 1991, and continues to evolve to keep pace with new developments in the field. In April 2002 the tool was awarded the prestigious System Software Award for 2001 by the ACM.

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.

Some Theorem Proving Strategies and their Implementation by shankar — last modified 2007-01-31 18:15

Original 1964 technical report by George A. Robinson, Lawrence T. Wos, and Daniel F. Carson describing their implementation on a CDC 3600 of J. A. Robinson's resolution method with unit preference and set-of-support strategies.

Maude 2.2 by shankar — last modified 2007-01-31 18:22

Maude is a high-performance reflective language and system supporting both equational and rewriting logic specification and programming for a wide range of applications. Maude has been influenced in important ways by the OBJ3 language, which can be regarded as an equational logic sublanguage. Besides supporting equational specification and programming, Maude also supports rewriting logic computation.