SNARK, (SRI's New Automated Reasoning Kit), is a
theorem prover for multi-sorted
first-order logic
First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantifie ...
intended for applications in
artificial intelligence
Artificial intelligence (AI) is intelligence—perceiving, synthesizing, and inferring information—demonstrated by machines, as opposed to intelligence displayed by animals and humans. Example tasks in which this is done include speech re ...
and
software engineering
Software engineering is a systematic engineering approach to software development.
A software engineer is a person who applies the principles of software engineering to design, develop, maintain, test, and evaluate computer software. The term '' ...
, developed at
SRI International
SRI International (SRI) is an American nonprofit scientific research institute and organization headquartered in Menlo Park, California. The trustees of Stanford University established SRI in 1946 as a center of innovation to support economic d ...
.
SNARK's principal inference mechanisms are
resolution
Resolution(s) may refer to:
Common meanings
* Resolution (debate), the statement which is debated in policy debate
* Resolution (law), a written motion adopted by a deliberative body
* New Year's resolution, a commitment that an individual mak ...
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
The National Aeronautics and Space Administration (NASA ) is an independent agency of the US federal government responsible for the civil space program, aeronautics research, and space research.
NASA was established in 1958, succeeding t ...
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
The Mozilla Public License (MPL) is a free and open-source weak copyleft license for most Mozilla Foundation software such as Firefox and Thunderbird The MPL license is developed and maintained by Mozilla, which seeks to balance the concerns ...
.
See also
*
Automated reasoning
*
Automated theorem proving
Automated theorem proving (also known as ATP or automated deduction) is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a maj ...
*
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
First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantifie ...
*
Formal verification
In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal metho ...
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