Artificial Intelligence White Papers
A Guide to SNARK
Overview 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 is a list of formulas. When a formula reaches the top of the agenda, SNARK will perform selected inferences involving tha
| Publisher | SRI International | File Format | HTML |
|---|---|---|---|
| Date Published | January 2001 | Downloads | 22 |
| Format | White Papers | ||
| Topics | |||
-
Did you find this white paper useful? 1 out of 2 users found this white paper useful
White Paper RSS
Download
Register
