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, 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.
- Automated reasoning
- Automated theorem proving
- Computer-aided proof
- First-order logic
- Formal verification
- 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.
|This scientific software article is a stub. You can help Wikipedia by expanding it.|