SNARK theorem prover
Encyclopedia
SNARK,, is a theorem prover for multi-sorted first-order logic
intended for applications in artificial intelligence
and software engineering
.
SNARK's principal inference mechanisms are resolution
and paramodulation; 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
and available under the Mozilla Public License
.
First-order logic
First-order logic is a formal logical system used in mathematics, philosophy, linguistics, and computer science. It goes by many names, including: first-order predicate calculus, the lower predicate calculus, quantification theory, and predicate logic...
intended for applications in artificial intelligence
Artificial intelligence
Artificial intelligence is the intelligence of machines and the branch of computer science that aims to create it. AI textbooks define the field as "the study and design of intelligent agents" where an intelligent agent is a system that perceives its environment and takes actions that maximize its...
and software engineering
Software engineering
Software Engineering is the application of a systematic, disciplined, quantifiable approach to the development, operation, and maintenance of software, and the study of these approaches; that is, the application of engineering to software...
.
SNARK's principal inference mechanisms are resolution
Resolution (logic)
In mathematical logic and automated theorem proving, resolution is a rule of inference leading to a refutation theorem-proving technique for sentences in propositional logic and first-order logic...
and paramodulation; 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
NASA
The National Aeronautics and Space Administration is the agency of the United States government that is responsible for the nation's civilian space program and for aeronautics and aerospace research...
Intelligent Systems Project. It is written in Common Lisp
Common Lisp
Common Lisp, commonly abbreviated CL, is a dialect of the Lisp programming language, published in ANSI standard document ANSI INCITS 226-1994 , . From the ANSI Common Lisp standard the Common Lisp HyperSpec has been derived for use with web browsers...
and available under the Mozilla Public License
Mozilla Public License
The Mozilla Public License is a free and open source software license. Version 1.0 was developed by Mitchell Baker when she worked as a lawyer at Netscape Communications Corporation and version 1.1 at the Mozilla Foundation...
.
See also
- Automated reasoningAutomated reasoningAutomated reasoning is an area of computer science dedicated to understand different aspects of reasoning. The study in automated reasoning helps produce software which allows computers to reason completely, or nearly completely, automatically...
- Automated theorem provingAutomated theorem provingAutomated theorem proving or automated deduction, currently the most well-developed subfield of automated reasoning , is the proving of mathematical theorems by a computer program.- Decidability of the problem :...
- Computer-aided proof
- First-order logicFirst-order logicFirst-order logic is a formal logical system used in mathematics, philosophy, linguistics, and computer science. It goes by many names, including: first-order predicate calculus, the lower predicate calculus, quantification theory, and predicate logic...
- Formal verificationFormal verificationIn 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 methods of mathematics .- Usage :Formal verification can be...