A Guide to SNARK

Introduction

Snark, SRI’s New Automated Reasoning Kit, is a theorem prover intended for applications in artificial intelligence and software engineering. Snark is geared toward dealing with large sets of assertions; it can be specialized with strategic controls that tune its performance; and it has facilities for integrating special purpose reasoning procedures with general-purpose inference. 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. It constitutes the deductive core of the NASA 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 a resolution-and-paramodulation theorem prover for first-order logic with equality—in this sense, it is in the same category as Argonne’s otter ([McCune]). Snark has provisions for both clausal and nonclausal reasoning, and it has an optional sort mechanism. It incorporates associative/commutative unification and a built-in decision procedure for reasoning about temporal points and intervals. It has no special facilities for proof by mathematical induction. It has some capabilities for abductive reasoning, which have been used in natural-language applications. Snark is implemented in an easily portable subset of common lisp. Snark is a refutation system; in other words, rather that trying to show directly that some assertions imply a desired conclusion, it attempts to show that the assertions and the negation of the conclusion imply a contradiction. It is an agenda-based system; that is, in seeking a refutation, it will put the assertions and the negation of the conclusion on an agenda. An agenda a list of formulas. When a formula reaches the top of the agenda, snark will perform selected inferences involving that formula and the previously processed formulas. The consequences of those inferences are added to the agenda. This process continues until the propositional symbol false is derived; this means that a contradiction has been deduced and the refutation is complete. The user has considerable control over the position at which a newly derived formula is placed on the agenda; this is one way in which a knowledgeable user can tailor snark’s search strategy to a particular application.

This document is an example-driven tutorial introduction to snark that will allow the reader to experiment with the system. It does not purport to introduce mathematical logic or resolution theorem proving; [Chang] provides an introduction to this style of theorem proving that does not assume any prior knowledge of logic. The guide also uses some notions introduced more fully in [Manna] and [Waldinger], particularly nonclausal resolution quantifier force, and answer extraction. Knowledge of lisp syntax and basics is also assumed here (e. g., see [Graham] or [Pitman]). Nevertheless, it is intended that a reader who is willing to suspend incomprehenension will be able to read this document without consulting other sources.