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, developed at SRI International.
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.
See also
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, 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