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 r ...
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 ...
.
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
The National Aeronautics and Space Administration (NASA ) is an independent agencies of the United States government, independent agency of the US federal government responsible for the civil List of government space agencies, space program ...
Intelligent Systems Project''. It is written in
Common Lisp 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
In computer science, in particular in knowledge representation and reasoning and metalogic, the area of automated reasoning is dedicated to understanding different aspects of reasoning. The study of automated reasoning helps produce computer prog ...
*
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 ma ...
*
Computer-aided proof
*
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 met ...
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, 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
The Association for the Advancement of Artificial Intelligence (AAAI) is an international scientific society devoted to promote research in, and responsible use of, artificial intelligence. AAAI also aims to increase public understanding of artif ...
, 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