SNARK theorem prover

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


Wikimedia Foundation. 2010.

Игры ⚽ Нужно решить контрольную?

Look at other dictionaries:

  • Snark — may refer to: *Snark (Lewis Carroll), a fictional animal in Lewis Carroll s The Hunting of the Snark (1876) *Jack London s yacht The Snark , described in the 1911 book The Cruise of the Snark *Snark (graph theory), a type of graph *SM 62 Snark,… …   Wikipedia

  • Automated theorem proving — (ATP) or automated deduction, currently the most well developed subfield of automated reasoning (AR), is the proving of mathematical theorems by a computer program. Decidability of the problem Depending on the underlying logic, the problem of… …   Wikipedia

  • List of mathematics articles (S) — NOTOC S S duality S matrix S plane S transform S unit S.O.S. Mathematics SA subgroup Saccheri quadrilateral Sacks spiral Sacred geometry Saddle node bifurcation Saddle point Saddle surface Sadleirian Professor of Pure Mathematics Safe prime Safe… …   Wikipedia

  • Richard Waldinger — Richard J. Waldinger is a computer science researcher at SRI Artificial Intelligence Laboratory (where he has worked since 1969) whose interests focus on the application of automated deductive reasoning to problems in software engineering and… …   Wikipedia

  • Demostración automática de teoremas — Saltar a navegación, búsqueda Para otros usos de este término, véase Demostración. La demostración automática de teoremas (de siglas ATP, por el término en inglés …   Wikipedia Español

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”