SNARK theorem prover

From Wikipedia, the free encyclopedia

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 NASA Intelligent Systems Project. It is written in Common Lisp and available under the Mozilla Public License.

[edit] 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, Jennifer Dungan. "Deductive Composition of Multiple Data Spources." [1]. May 2002 Progress Report of the Intelligent Data Understanding Research Task, Intelligent System Project, NASA SISM.
Waldinger, R. and Appelt, D. E. and Fry, J. and Israel, D. J. and Jarvis, P. and Martin, D. and Riehemann, S. and Stickel, M. E. and Tyson, M. and Hobbs, J. and Dungan, J. L. "Deductive Question Answering from Multiple Resources." in New Directions in Question Answering, AAAI, 2004. [2]
Waldinger, R. , Jarvis, P., and Dungan, J. "Using Deduction to Choreograph Multiple Data Sources." In Semantic Web Technologies for Searching and Retrieving, Sanibel Island, Florida, Oct 2003.