SNARK theorem prover

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.

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 [http://is.arc.nasa.gov/index.html NASA Intelligent Systems Project] . It is written in Common Lisp and available under the Mozilla Public License.

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, 341–355.
* Richard Waldinger, Martin Reddy, and Jennifer Dungan. "Deductive Composition of Multiple Data Spources." [http://is.arc.nasa.gov/IDU/slides/reports02/DedCmp02b.pdf] . 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. [http://www.ai.sri.com/pubs/files/986.pdf]
* 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

* [http://www.ai.sri.com/~stickel/snark.html SNARK homepage at SRI]
* [http://www.ai.sri.com/snark/tutorial/tutorial.html SNARK tutorial]

See also

* Automated theorem proving
* Computer-aided proof
* Automated reasoning
* Formal verification
* First-order logic