SNARK - SRI's New Automated Reasoning Kit

Overview

SNARK is an automated theorem-proving program being developed in Common Lisp. Its principal inference rules are resolution and paramodulation. SNARK's style of theorem proving is similar to Otter's.

Some distinctive features of SNARK are its support for special unification algorithms, sorts, nonclausal formulas, answer construction for program synthesis, procedural attachment, and extensibility by Lisp code.

SNARK has been used as the reasoning component of SRI's High Performance Knowledge Base (HPKB) system, which deduces answers to questions based on large repositories of information, and as the deductive core of NASA's Amphion system, which composes software from components to meet users' specifications, e.g., to perform computations in planetary astronomy. SNARK has also been connected to Kestrel's SPECWARE environment for software development.

SNARK is now available under the terms of the Mozilla Public License. Note that SNARK is still largely unfinished, undocumented, and unsupported. It can be downloaded here.

A Guide to SNARK is being written. Send comments to Richard Waldinger (waldinger@ai.sri.com).

The TPTP Problem Library is a source of problems for evaluating and comparing automated theorem-proving programs. Results for SNARK on the TPTP problem set are available here.

Selected Publications

• Stickel, M., R. Waldinger, M. Lowry, T. Pressburger, and I. Underwood. Deductive composition of astronomical software from subroutine libraries. Proceedings of the Twelfth International Conference on Automated Deduction (CADE-12), Nancy, France, June 1994, 341-355.

Some Related Systems

• Amphion - Knowledge-Based Software Engineering
• Otter, by William McCune (mccune@mcs.anl.gov)
• Automated Reasoning Systems Database lists additional automated reasoning systems