SNARK, (SRI's New Automated Reasoning Kit), is a
theorem prover for multi-sorted
first-order logic intended for applications in
artificial intelligence and
software engineering, developed at
SRI International.
SNARK's principal inference mechanisms are
resolution and
paramodulation
In mathematical logic and automated theorem proving, resolution is a rule of inference leading to a refutation complete theorem-proving technique for sentences in propositional logic and first-order logic. For propositional logic, systematically ...
; in addition it offers specialized decision procedures for particular domains, e.g., a constraint solver for Allen's temporal interval logic. In contrast to many other theorem provers is fully automated (non-interactive). SNARK offers many strategic controls for adjusting its search behavior and thus tune its performance to particular applications. This, together with its use of multi-sorted logic and facilities for integrating special-purpose reasoning procedures with general-purpose inference make it particularly suited as reasoner for large sets of assertions.
SNARK is used as reasoning component in the ''
NASA Intelligent Systems Project''. It is written in
Common Lisp
Common Lisp (CL) is a dialect of the Lisp programming language, published in ANSI standard document ''ANSI INCITS 226-1994 (S20018)'' (formerly ''X3.226-1994 (R1999)''). The Common Lisp HyperSpec, a hyperlinked HTML version, has been derived fro ...
and available under the
Mozilla Public License.
See also
*
Automated reasoning
*
Automated theorem proving
*
Computer-aided proof
A computer-assisted proof is a mathematical proof that has been at least partially generated by computer.
Most computer-aided proofs to date have been implementations of large proofs-by-exhaustion of a mathematical theorem. The idea is to use a ...
*
First-order logic
*
Formal verification
References
* M. Stickel,
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, pages 341–355.
*
Richard Waldinger
Richard Jay Waldinger is a computer science researcher at SRI International's Artificial Intelligence Center (where he has worked since 1969) whose interests focus on the application of automated deductive reasoning to problems in software enginee ...
, Martin Reddy, and Jennifer Dungan.
Deductive Composition of Multiple Data Sources. May 2002 Progress Report of the Intelligent Data Understanding Research Task, Intelligent System Project, NASA SISM.
*
R, Waldinger, D. E. Appelt, J. Fry, D. J. Israel, P. Jarvis, D. Martin, S. Riehemann, M. E. Stickel, M. Tyson, J. Hobbs, and J. L. Dungan.
Deductive Question Answering from Multiple Resources. in ''New Directions in Question Answering'',
AAAI, 2004.
*
R. Waldinger, P. Jarvis, and J. Dungan. "Using Deduction to Choreograph Multiple Data Sources." In ''Semantic Web Technologies for Searching and Retrieving'', Sanibel Island, Florida, October 2003.
External links
SNARK homepage at SRI
Free theorem provers
Common Lisp (programming language) software
SRI International software
{{science-software-stub