• Skip to primary navigation
  • Skip to main content
SRI logo
  • About
    • Press room
    • Our history
  • Expertise
    • Advanced imaging systems
    • Artificial intelligence
    • Biomedical R&D services
    • Biomedical sciences
    • Computer vision
    • Cyber & formal methods
    • Education and learning
    • Innovation strategy and policy
    • National security
    • Ocean & space
    • Quantum
    • QED-C
    • Robotics, sensors & devices
    • Speech & natural language
    • Video test & measurement
  • Ventures
  • NSIC
  • Careers
  • Contact
  • 日本支社
Search
Close
Artificial intelligence publications May 1, 2000

A Guide to SNARK

Citation

Copy to clipboard


Stickel, Mark & Waldinger, Richard & Chaudhri, Vinay. (2000). A Guide to SNARK.

Introduction

Snark, SRI’s New Automated Reasoning Kit, is a theorem prover intended for applications in artificial intelligence and software engineering. Snark is geared toward dealing with large sets of assertions; it can be specialized with strategic controls that tune its performance; and it has facilities for integrating special purpose reasoning procedures with general-purpose inference. Snark has been used as the reasoning component of SRI’s High Performance Knowledge Base (HPKB) system, which deduces answers to questions based on large repositories of information. It constitutes the deductive core of the NASA Amphion system, which composes software from components to meet users’ specifications, e. g., to perform computations in planetary astronomy. Snark has also been connected to Kestrel’s specware environment for software development.


Snark is a resolution-and-paramodulation theorem prover for first-order logic with equality—in this sense, it is in the same category as Argonne’s otter ([McCune]). Snark has provisions for both clausal and nonclausal reasoning, and it has an optional sort mechanism. It incorporates associative/commutative unification and a built-in decision procedure for reasoning about temporal points and intervals. It has no special facilities for proof by mathematical induction. It has some capabilities for abductive reasoning, which have been used in natural-language applications. Snark is implemented in an easily portable subset of common lisp. Snark is a refutation system; in other words, rather that trying to show directly that some assertions imply a desired conclusion, it attempts to show that the assertions and the negation of the conclusion imply a contradiction. It is an agenda-based system; that is, in seeking a refutation, it will put the assertions and the negation of the conclusion on an agenda. An agenda a list of formulas. When a formula reaches the top of the agenda, snark will perform selected inferences involving that formula and the previously processed formulas. The consequences of those inferences are added to the agenda. This process continues until the propositional symbol false is derived; this means that a contradiction has been deduced and the refutation is complete. The user has considerable control over the position at which a newly derived formula is placed on the agenda; this is one way in which a knowledgeable user can tailor snark’s search strategy to a particular application.

This document is an example-driven tutorial introduction to snark that will allow the reader to experiment with the system. It does not purport to introduce mathematical logic or resolution theorem proving; [Chang] provides an introduction to this style of theorem proving that does not assume any prior knowledge of logic. The guide also uses some notions introduced more fully in [Manna] and [Waldinger], particularly nonclausal resolution quantifier force, and answer extraction. Knowledge of lisp syntax and basics is also assumed here (e. g., see [Graham] or [Pitman]). Nevertheless, it is intended that a reader who is willing to suspend incomprehenension will be able to read this document without consulting other sources.

↓ Download

Share this

How can we help?

Once you hit send…

We’ll match your inquiry to the person who can best help you.

Expect a response within 48 hours.

Career call to action image

Make your own mark.

Search jobs

Our work

Case studies

Publications

Timeline of innovation

Areas of expertise

Institute

Leadership

Press room

Media inquiries

Compliance

Careers

Job listings

Contact

SRI Ventures

Our locations

Headquarters

333 Ravenswood Ave
Menlo Park, CA 94025 USA

+1 (650) 859-2000

Subscribe to our newsletter


日本支社
SRI International
  • Contact us
  • Privacy Policy
  • Cookies
  • DMCA
  • Copyright © 2022 SRI International