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.
Selected Publications
Some Related Systems
- SNARK, another reasoning system with the same name by Jean-Louis Laurière in 1985,
is described in J.-L. Laurière and M. Vialatte,
SNARK: A Language to Represent Declarative Knowledge and an Inference Engine which Uses Heuristics,
Proceedings of the IFIP Congress, 1986, 811-816.
- Amphion - Knowledge-Based Software Engineering
- Otter,
by William McCune
- Automated Reasoning Systems Database
lists additional automated reasoning systems
Downloads
- SNARK is now available under the terms of the
Mozilla Public License.
Note that SNARK is still largely unfinished, undocumented, and unsupported.
- Current version
- Earlier version snark-20050129l
- Earlier version snark-20031012g
- A Guide to SNARK
has been written but not updated yet to reflect changes in SNARK,
especially for sorts and temporal and spatial reasoning.
- 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.
Mark E. Stickel (stickel
ai.sri.com)
2007-02-15