SNARK - SRI’s New Automated Reasoning Kit. SNARK is an automated theorem-proving program being developed in Common Lisp. Its principal inference rules are resolution and paramodulation. SNARK’s style of theorem proving is similar to Otter’s. Some distinctive features of SNARK are its support for special unification algorithms, sorts, answer construction for program synthesis, procedural attachment, and extensibility by Lisp code. 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, and as the deductive core of NASA’s 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.
Keywords for this software
References in zbMATH (referenced in 4 articles )
Showing results 1 to 4 of 4.
- Govindarajalulu, Naveen Sundar; Bringsjord, Selmer; Taylor, Joshua: Proof verification and proof discovery for relativity (2015)
- Schulz, Stephan: Simple and efficient clause subsumption with feature vector indexing (2013)
- Sutcliffe, Geoff: The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0 (2009)
- Roach, Steve; Van Baalen, Jeffrey: Automated procedure construction for deductive synthesis (2005) ioport