Next: Introduction, Previous: (dir), Up: (dir) [Contents][Index]
This is the snark Reference Manual, generated automatically by Declt version 2.4 "Will Decker" on Wed Jun 20 12:35:48 2018 GMT+0.
| • Introduction: | What snark is all about | |
| • Systems: | The systems documentation | |
| • Files: | The files documentation | |
| • Packages: | The packages documentation | |
| • Definitions: | The symbols documentation | |
| • Indexes: | Concepts, functions, variables and data types |
=====
SNARK
=====
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.
--------
Overview
--------
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.
Selected Publications
Stickel, M., 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.
---------------------
Links & Documentation
---------------------
SNARK tutorial ... http://www.ai.sri.com/snark/tutorial/tutorial.html
SNARK paper ...... http://www.sri.com/work/publications/guide-snark
SNARK home ....... http://www.ai.sri.com/~stickel/snark.html
SNARK author ..... https://en.wikipedia.org/wiki/Mark_E._Stickel
----------------
Obtaining SNARK:
----------------
New (18-MAR-2016): get it by QuickLisp
(ql:quickload :snark)
Or:
SNARK can be downloaded from the SNARK web page
http://www.ai.sri.com/~stickel/snark.html
See INSTALL file for installation instructions
Running SNARK:
lisp
(load "snark-system.lisp")
(make-snark-system)
:
Examples:
(overbeek-test) in overbeek-test.lisp
some standard theorem-proving examples, some time-consuming
(steamroller-example) in steamroller-example.lisp
illustrates sorts
(front-last-example) in front-last-example.lisp
illustrates program synthesis
(reverse-example) in reverse-example.lisp
illustrates logic programming style usage
A guide to SNARK has been written:
http://www.ai.sri.com/snark/tutorial/tutorial.html
but has not been updated yet to reflect changes in SNARK,
especially for temporal and spatial reasoning.
-----
NOTES
-----
This repository is based on the latest version 20120808-r022 from the
download site and the '.asd' files from https://github.com/hoelzl/Snark.
The goal is to get SNARK installable by QuickLisp.
Loadable by quicklisp since: 18-MAR-2016
* (ql:system-apropos :snark)
#
#
#
#
#
#
#
#
#
#
#
#
#
#
*
Next: Files, Previous: Introduction, Up: Top [Contents][Index]
The main system appears first, followed by any subsystem dependency.
Next: The snark-implementation system, Previous: Systems, Up: Systems [Contents][Index]
Mark E. Stickel, SRI International
MPL 1.1, see file LICENSE
The Snark Theorem Prover
snark-implementation (system)
snark.asd (file)
Next: The snark-numbering system, Previous: The snark system, Up: Systems [Contents][Index]
Mark E. Stickel, SRI International
MPL 1.1, see file LICENSE
The Snark Theorem Prover
snark-implementation.asd (file)
Next: The snark-agenda system, Previous: The snark-implementation system, Up: Systems [Contents][Index]
Mark E. Stickel, SRI International
MPL 1.1, see file LICENSE
The Snark Theorem Prover
snark-numbering.asd (file)
numbering.lisp (file)
Next: The snark-deque system, Previous: The snark-numbering system, Up: Systems [Contents][Index]
Mark E. Stickel, SRI International
MPL 1.1, see file LICENSE
The Snark Theorem Prover
snark-agenda.asd (file)
agenda.lisp (file)
Next: The snark-sparse-array system, Previous: The snark-agenda system, Up: Systems [Contents][Index]
Mark E. Stickel, SRI International
MPL 1.1, see file LICENSE
The Snark Theorem Prover
snark-deque.asd (file)
deque2.lisp (file)
Next: The snark-feature system, Previous: The snark-deque system, Up: Systems [Contents][Index]
Mark E. Stickel, SRI International
MPL 1.1, see file LICENSE
The Snark Theorem Prover
snark-sparse-array.asd (file)
Next: The snark-infix-reader system, Previous: The snark-sparse-array system, Up: Systems [Contents][Index]
Mark E. Stickel, SRI International
MPL 1.1, see file LICENSE
The Snark Theorem Prover
snark-feature.asd (file)
feature.lisp (file)
Next: The snark-pkg system, Previous: The snark-feature system, Up: Systems [Contents][Index]
Mark E. Stickel, SRI International
MPL 1.1, see file LICENSE
The Snark Theorem Prover
snark-infix-reader.asd (file)
Next: The snark-dpll system, Previous: The snark-infix-reader system, Up: Systems [Contents][Index]
Mark E. Stickel, SRI International
MPL 1.1, see file LICENSE
The Snark Theorem Prover
snark-dpll (system)
snark-pkg.asd (file)
snark-pkg.lisp (file)
Next: The snark-lisp system, Previous: The snark-pkg system, Up: Systems [Contents][Index]
Mark E. Stickel, SRI International
MPL 1.1, see file LICENSE
The Snark Theorem Prover
snark-dpll.asd (file)
davis-putnam3.lisp (file)
Next: The snark-auxiliary-packages system, Previous: The snark-dpll system, Up: Systems [Contents][Index]
Mark E. Stickel, SRI International
MPL 1.1, see file LICENSE
The Snark Theorem Prover
snark-auxiliary-packages (system)
snark-lisp.asd (file)
Previous: The snark-lisp system, Up: Systems [Contents][Index]
Mark E. Stickel, SRI International
MPL 1.1, see file LICENSE
The Snark Theorem Prover
snark-auxiliary-packages.asd (file)
auxiliary-packages.lisp (file)
Files are sorted by type and then listed depth-first from the systems components trees.
| • Lisp files: |
Next: The snark-implementation<dot>asd file, Previous: Lisp files, Up: Lisp files [Contents][Index]
snark.asd
snark (system)
Next: The snark-numbering<dot>asd file, Previous: The snark<dot>asd file, Up: Lisp files [Contents][Index]
snark-implementation.asd
snark-implementation (system)
Next: The snark-agenda<dot>asd file, Previous: The snark-implementation<dot>asd file, Up: Lisp files [Contents][Index]
snark-numbering.asd
snark-numbering (system)
Next: The snark-deque<dot>asd file, Previous: The snark-numbering<dot>asd file, Up: Lisp files [Contents][Index]
snark-agenda.asd
snark-agenda (system)
Next: The snark-sparse-array<dot>asd file, Previous: The snark-agenda<dot>asd file, Up: Lisp files [Contents][Index]
snark-deque.asd
snark-deque (system)
Next: The snark-feature<dot>asd file, Previous: The snark-deque<dot>asd file, Up: Lisp files [Contents][Index]
snark-sparse-array.asd
snark-sparse-array (system)
Next: The snark-infix-reader<dot>asd file, Previous: The snark-sparse-array<dot>asd file, Up: Lisp files [Contents][Index]
snark-feature.asd
snark-feature (system)
Next: The snark-pkg<dot>asd file, Previous: The snark-feature<dot>asd file, Up: Lisp files [Contents][Index]
snark-infix-reader.asd
snark-infix-reader (system)
Next: The snark-dpll<dot>asd file, Previous: The snark-infix-reader<dot>asd file, Up: Lisp files [Contents][Index]
snark-pkg.asd
snark-pkg (system)
Next: The snark-lisp<dot>asd file, Previous: The snark-pkg<dot>asd file, Up: Lisp files [Contents][Index]
snark-dpll.asd
snark-dpll (system)
Next: The snark-auxiliary-packages<dot>asd file, Previous: The snark-dpll<dot>asd file, Up: Lisp files [Contents][Index]
snark-lisp.asd
snark-lisp (system)
Next: The snark-implementation/useful<dot>lisp file, Previous: The snark-lisp<dot>asd file, Up: Lisp files [Contents][Index]
snark-auxiliary-packages.asd
snark-auxiliary-packages (system)
Next: The snark-implementation/posets<dot>lisp file, Previous: The snark-auxiliary-packages<dot>asd file, Up: Lisp files [Contents][Index]
snark-implementation (system)
src/useful.lisp
Next: The snark-implementation/solve-sum<dot>lisp file, Previous: The snark-implementation/useful<dot>lisp file, Up: Lisp files [Contents][Index]
useful.lisp (file)
snark-implementation (system)
src/posets.lisp
Next: The snark-implementation/globals<dot>lisp file, Previous: The snark-implementation/posets<dot>lisp file, Up: Lisp files [Contents][Index]
posets.lisp (file)
snark-implementation (system)
src/solve-sum.lisp
Next: The snark-implementation/options<dot>lisp file, Previous: The snark-implementation/solve-sum<dot>lisp file, Up: Lisp files [Contents][Index]
solve-sum.lisp (file)
snark-implementation (system)
src/globals.lisp
Next: The snark-implementation/terms2<dot>lisp file, Previous: The snark-implementation/globals<dot>lisp file, Up: Lisp files [Contents][Index]
globals.lisp (file)
snark-implementation (system)
src/options.lisp
Next: The snark-implementation/rows<dot>lisp file, Previous: The snark-implementation/options<dot>lisp file, Up: Lisp files [Contents][Index]
options.lisp (file)
snark-implementation (system)
src/terms2.lisp
Next: The snark-implementation/row-contexts<dot>lisp file, Previous: The snark-implementation/terms2<dot>lisp file, Up: Lisp files [Contents][Index]
terms2.lisp (file)
snark-implementation (system)
src/rows.lisp
Next: The snark-implementation/constants<dot>lisp file, Previous: The snark-implementation/rows<dot>lisp file, Up: Lisp files [Contents][Index]
rows.lisp (file)
snark-implementation (system)
src/row-contexts.lisp
Next: The snark-implementation/functions<dot>lisp file, Previous: The snark-implementation/row-contexts<dot>lisp file, Up: Lisp files [Contents][Index]
row-contexts.lisp (file)
snark-implementation (system)
src/constants.lisp
Next: The snark-implementation/variables<dot>lisp file, Previous: The snark-implementation/constants<dot>lisp file, Up: Lisp files [Contents][Index]
constants.lisp (file)
snark-implementation (system)
src/functions.lisp
Next: The snark-implementation/subst<dot>lisp file, Previous: The snark-implementation/functions<dot>lisp file, Up: Lisp files [Contents][Index]
functions.lisp (file)
snark-implementation (system)
src/variables.lisp
Next: The snark-implementation/substitute<dot>lisp file, Previous: The snark-implementation/variables<dot>lisp file, Up: Lisp files [Contents][Index]
variables.lisp (file)
snark-implementation (system)
src/subst.lisp
Next: The snark-implementation/symbol-table2<dot>lisp file, Previous: The snark-implementation/subst<dot>lisp file, Up: Lisp files [Contents][Index]
subst.lisp (file)
snark-implementation (system)
src/substitute.lisp
Next: The snark-implementation/symbol-definitions<dot>lisp file, Previous: The snark-implementation/substitute<dot>lisp file, Up: Lisp files [Contents][Index]
substitute.lisp (file)
snark-implementation (system)
src/symbol-table2.lisp
Next: The snark-implementation/assertion-analysis<dot>lisp file, Previous: The snark-implementation/symbol-table2<dot>lisp file, Up: Lisp files [Contents][Index]
symbol-table2.lisp (file)
snark-implementation (system)
src/symbol-definitions.lisp
Next: The snark-implementation/jepd-relations-tables<dot>lisp file, Previous: The snark-implementation/symbol-definitions<dot>lisp file, Up: Lisp files [Contents][Index]
symbol-definitions.lisp (file)
snark-implementation (system)
src/assertion-analysis.lisp
Next: The snark-implementation/jepd-relations<dot>lisp file, Previous: The snark-implementation/assertion-analysis<dot>lisp file, Up: Lisp files [Contents][Index]
assertion-analysis.lisp (file)
snark-implementation (system)
src/jepd-relations-tables.lisp
Next: The snark-implementation/date-reasoning2<dot>lisp file, Previous: The snark-implementation/jepd-relations-tables<dot>lisp file, Up: Lisp files [Contents][Index]
jepd-relations-tables.lisp (file)
snark-implementation (system)
src/jepd-relations.lisp
Next: The snark-implementation/constraints<dot>lisp file, Previous: The snark-implementation/jepd-relations<dot>lisp file, Up: Lisp files [Contents][Index]
jepd-relations.lisp (file)
snark-implementation (system)
src/date-reasoning2.lisp
Next: The snark-implementation/constraint-purify<dot>lisp file, Previous: The snark-implementation/date-reasoning2<dot>lisp file, Up: Lisp files [Contents][Index]
date-reasoning2.lisp (file)
snark-implementation (system)
src/constraints.lisp
Next: The snark-implementation/connectives<dot>lisp file, Previous: The snark-implementation/constraints<dot>lisp file, Up: Lisp files [Contents][Index]
constraints.lisp (file)
snark-implementation (system)
src/constraint-purify.lisp
Next: The snark-implementation/wffs<dot>lisp file, Previous: The snark-implementation/constraint-purify<dot>lisp file, Up: Lisp files [Contents][Index]
constraint-purify.lisp (file)
snark-implementation (system)
src/connectives.lisp
Next: The snark-implementation/nonhorn-magic-set<dot>lisp file, Previous: The snark-implementation/connectives<dot>lisp file, Up: Lisp files [Contents][Index]
connectives.lisp (file)
snark-implementation (system)
src/wffs.lisp
Next: The snark-implementation/dp-refute<dot>lisp file, Previous: The snark-implementation/wffs<dot>lisp file, Up: Lisp files [Contents][Index]
wffs.lisp (file)
snark-implementation (system)
src/nonhorn-magic-set.lisp
Next: The snark-implementation/sorts-functions<dot>lisp file, Previous: The snark-implementation/nonhorn-magic-set<dot>lisp file, Up: Lisp files [Contents][Index]
nonhorn-magic-set.lisp (file)
snark-implementation (system)
src/dp-refute.lisp
Next: The snark-implementation/sorts-interface<dot>lisp file, Previous: The snark-implementation/dp-refute<dot>lisp file, Up: Lisp files [Contents][Index]
dp-refute.lisp (file)
snark-implementation (system)
src/sorts-functions.lisp
Next: The snark-implementation/sorts<dot>lisp file, Previous: The snark-implementation/sorts-functions<dot>lisp file, Up: Lisp files [Contents][Index]
sorts-functions.lisp (file)
snark-implementation (system)
src/sorts-interface.lisp
Next: The snark-implementation/argument-bag-ac<dot>lisp file, Previous: The snark-implementation/sorts-interface<dot>lisp file, Up: Lisp files [Contents][Index]
sorts-interface.lisp (file)
snark-implementation (system)
src/sorts.lisp
term-sort (function)
Next: The snark-implementation/argument-list-a1<dot>lisp file, Previous: The snark-implementation/sorts<dot>lisp file, Up: Lisp files [Contents][Index]
sorts.lisp (file)
snark-implementation (system)
src/argument-bag-ac.lisp
Next: The snark-implementation/unify<dot>lisp file, Previous: The snark-implementation/argument-bag-ac<dot>lisp file, Up: Lisp files [Contents][Index]
argument-bag-ac.lisp (file)
snark-implementation (system)
src/argument-list-a1.lisp
Next: The snark-implementation/unify-bag<dot>lisp file, Previous: The snark-implementation/argument-list-a1<dot>lisp file, Up: Lisp files [Contents][Index]
argument-list-a1.lisp (file)
snark-implementation (system)
src/unify.lisp
unify (function)
Next: The snark-implementation/subsume-bag<dot>lisp file, Previous: The snark-implementation/unify<dot>lisp file, Up: Lisp files [Contents][Index]
unify.lisp (file)
snark-implementation (system)
src/unify-bag.lisp
Next: The snark-implementation/unify-vector<dot>lisp file, Previous: The snark-implementation/unify-bag<dot>lisp file, Up: Lisp files [Contents][Index]
unify-bag.lisp (file)
snark-implementation (system)
src/subsume-bag.lisp
Next: The snark-implementation/equal<dot>lisp file, Previous: The snark-implementation/subsume-bag<dot>lisp file, Up: Lisp files [Contents][Index]
subsume-bag.lisp (file)
snark-implementation (system)
src/unify-vector.lisp
Next: The snark-implementation/variant<dot>lisp file, Previous: The snark-implementation/unify-vector<dot>lisp file, Up: Lisp files [Contents][Index]
unify-vector.lisp (file)
snark-implementation (system)
src/equal.lisp
equal-p (function)
Next: The snark-implementation/alists<dot>lisp file, Previous: The snark-implementation/equal<dot>lisp file, Up: Lisp files [Contents][Index]
equal.lisp (file)
snark-implementation (system)
src/variant.lisp
Next: The snark-implementation/term-hash<dot>lisp file, Previous: The snark-implementation/variant<dot>lisp file, Up: Lisp files [Contents][Index]
variant.lisp (file)
snark-implementation (system)
src/alists.lisp
Next: The snark-implementation/trie-index<dot>lisp file, Previous: The snark-implementation/alists<dot>lisp file, Up: Lisp files [Contents][Index]
alists.lisp (file)
snark-implementation (system)
src/term-hash.lisp
Next: The snark-implementation/path-index<dot>lisp file, Previous: The snark-implementation/term-hash<dot>lisp file, Up: Lisp files [Contents][Index]
term-hash.lisp (file)
snark-implementation (system)
src/trie-index.lisp
Next: The snark-implementation/trie<dot>lisp file, Previous: The snark-implementation/trie-index<dot>lisp file, Up: Lisp files [Contents][Index]
trie-index.lisp (file)
snark-implementation (system)
src/path-index.lisp
Next: The snark-implementation/feature-vector<dot>lisp file, Previous: The snark-implementation/path-index<dot>lisp file, Up: Lisp files [Contents][Index]
path-index.lisp (file)
snark-implementation (system)
src/trie.lisp
Next: The snark-implementation/feature-vector-trie<dot>lisp file, Previous: The snark-implementation/trie<dot>lisp file, Up: Lisp files [Contents][Index]
trie.lisp (file)
snark-implementation (system)
src/feature-vector.lisp
Next: The snark-implementation/feature-vector-index<dot>lisp file, Previous: The snark-implementation/feature-vector<dot>lisp file, Up: Lisp files [Contents][Index]
feature-vector.lisp (file)
snark-implementation (system)
src/feature-vector-trie.lisp
Next: The snark-implementation/term-memory<dot>lisp file, Previous: The snark-implementation/feature-vector-trie<dot>lisp file, Up: Lisp files [Contents][Index]
feature-vector-trie.lisp (file)
snark-implementation (system)
src/feature-vector-index.lisp
Next: The snark-implementation/weight<dot>lisp file, Previous: The snark-implementation/feature-vector-index<dot>lisp file, Up: Lisp files [Contents][Index]
feature-vector-index.lisp (file)
snark-implementation (system)
src/term-memory.lisp
Next: The snark-implementation/eval<dot>lisp file, Previous: The snark-implementation/term-memory<dot>lisp file, Up: Lisp files [Contents][Index]
term-memory.lisp (file)
snark-implementation (system)
src/weight.lisp
Next: The snark-implementation/input<dot>lisp file, Previous: The snark-implementation/weight<dot>lisp file, Up: Lisp files [Contents][Index]
weight.lisp (file)
snark-implementation (system)
src/eval.lisp
Next: The snark-implementation/output<dot>lisp file, Previous: The snark-implementation/eval<dot>lisp file, Up: Lisp files [Contents][Index]
eval.lisp (file)
snark-implementation (system)
src/input.lisp
Next: The snark-implementation/simplification-ordering<dot>lisp file, Previous: The snark-implementation/input<dot>lisp file, Up: Lisp files [Contents][Index]
input.lisp (file)
snark-implementation (system)
src/output.lisp
Next: The snark-implementation/symbol-ordering<dot>lisp file, Previous: The snark-implementation/output<dot>lisp file, Up: Lisp files [Contents][Index]
output.lisp (file)
snark-implementation (system)
src/simplification-ordering.lisp
Next: The snark-implementation/multiset-ordering<dot>lisp file, Previous: The snark-implementation/simplification-ordering<dot>lisp file, Up: Lisp files [Contents][Index]
simplification-ordering.lisp (file)
snark-implementation (system)
src/symbol-ordering.lisp
Next: The snark-implementation/recursive-path-ordering<dot>lisp file, Previous: The snark-implementation/symbol-ordering<dot>lisp file, Up: Lisp files [Contents][Index]
symbol-ordering.lisp (file)
snark-implementation (system)
src/multiset-ordering.lisp
Next: The snark-implementation/ac-rpo<dot>lisp file, Previous: The snark-implementation/multiset-ordering<dot>lisp file, Up: Lisp files [Contents][Index]
multiset-ordering.lisp (file)
snark-implementation (system)
src/recursive-path-ordering.lisp
Next: The snark-implementation/knuth-bendix-ordering2<dot>lisp file, Previous: The snark-implementation/recursive-path-ordering<dot>lisp file, Up: Lisp files [Contents][Index]
recursive-path-ordering.lisp (file)
snark-implementation (system)
src/ac-rpo.lisp
Next: The snark-implementation/rewrite<dot>lisp file, Previous: The snark-implementation/ac-rpo<dot>lisp file, Up: Lisp files [Contents][Index]
ac-rpo.lisp (file)
snark-implementation (system)
src/knuth-bendix-ordering2.lisp
Next: The snark-implementation/rewrite-code<dot>lisp file, Previous: The snark-implementation/knuth-bendix-ordering2<dot>lisp file, Up: Lisp files [Contents][Index]
knuth-bendix-ordering2.lisp (file)
snark-implementation (system)
src/rewrite.lisp
rewrite (structure)
Next: The snark-implementation/code-for-strings2<dot>lisp file, Previous: The snark-implementation/rewrite<dot>lisp file, Up: Lisp files [Contents][Index]
rewrite.lisp (file)
snark-implementation (system)
src/rewrite-code.lisp
declare-cancellation-law (function)
Next: The snark-implementation/code-for-numbers3<dot>lisp file, Previous: The snark-implementation/rewrite-code<dot>lisp file, Up: Lisp files [Contents][Index]
rewrite-code.lisp (file)
snark-implementation (system)
src/code-for-strings2.lisp
Next: The snark-implementation/code-for-lists2<dot>lisp file, Previous: The snark-implementation/code-for-strings2<dot>lisp file, Up: Lisp files [Contents][Index]
code-for-strings2.lisp (file)
snark-implementation (system)
src/code-for-numbers3.lisp
Next: The snark-implementation/code-for-bags4<dot>lisp file, Previous: The snark-implementation/code-for-numbers3<dot>lisp file, Up: Lisp files [Contents][Index]
code-for-numbers3.lisp (file)
snark-implementation (system)
src/code-for-lists2.lisp
declare-code-for-lists (function)
Next: The snark-implementation/resolve-code<dot>lisp file, Previous: The snark-implementation/code-for-lists2<dot>lisp file, Up: Lisp files [Contents][Index]
code-for-lists2.lisp (file)
snark-implementation (system)
src/code-for-bags4.lisp
Next: The snark-implementation/resolve-code-tables<dot>lisp file, Previous: The snark-implementation/code-for-bags4<dot>lisp file, Up: Lisp files [Contents][Index]
code-for-bags4.lisp (file)
snark-implementation (system)
src/resolve-code.lisp
Next: The snark-implementation/main<dot>lisp file, Previous: The snark-implementation/resolve-code<dot>lisp file, Up: Lisp files [Contents][Index]
resolve-code.lisp (file)
snark-implementation (system)
src/resolve-code-tables.lisp
Next: The snark-implementation/subsume<dot>lisp file, Previous: The snark-implementation/resolve-code-tables<dot>lisp file, Up: Lisp files [Contents][Index]
resolve-code-tables.lisp (file)
snark-implementation (system)
src/main.lisp
Next: The snark-implementation/subsume-clause<dot>lisp file, Previous: The snark-implementation/main<dot>lisp file, Up: Lisp files [Contents][Index]
main.lisp (file)
snark-implementation (system)
src/subsume.lisp
Next: The snark-implementation/interactive<dot>lisp file, Previous: The snark-implementation/subsume<dot>lisp file, Up: Lisp files [Contents][Index]
subsume.lisp (file)
snark-implementation (system)
src/subsume-clause.lisp
Next: The snark-implementation/assertion-file<dot>lisp file, Previous: The snark-implementation/subsume-clause<dot>lisp file, Up: Lisp files [Contents][Index]
subsume-clause.lisp (file)
snark-implementation (system)
src/interactive.lisp
Next: The snark-implementation/tptp<dot>lisp file, Previous: The snark-implementation/interactive<dot>lisp file, Up: Lisp files [Contents][Index]
interactive.lisp (file)
snark-implementation (system)
src/assertion-file.lisp
Next: The snark-implementation/tptp-symbols<dot>lisp file, Previous: The snark-implementation/assertion-file<dot>lisp file, Up: Lisp files [Contents][Index]
assertion-file.lisp (file)
snark-implementation (system)
src/tptp.lisp
Next: The snark-implementation/coder<dot>lisp file, Previous: The snark-implementation/tptp<dot>lisp file, Up: Lisp files [Contents][Index]
tptp.lisp (file)
snark-implementation (system)
src/tptp-symbols.lisp
declare-tptp-sort (function)
Next: The snark-numbering/numbering<dot>lisp file, Previous: The snark-implementation/tptp-symbols<dot>lisp file, Up: Lisp files [Contents][Index]
tptp-symbols.lisp (file)
snark-implementation (system)
src/coder.lisp
Next: The snark-agenda/agenda<dot>lisp file, Previous: The snark-implementation/coder<dot>lisp file, Up: Lisp files [Contents][Index]
snark-numbering (system)
src/numbering.lisp
*nonce* (special variable)
Next: The snark-deque/deque2<dot>lisp file, Previous: The snark-numbering/numbering<dot>lisp file, Up: Lisp files [Contents][Index]
snark-agenda (system)
src/agenda.lisp
Next: The snark-sparse-array/sparse-vector5<dot>lisp file, Previous: The snark-agenda/agenda<dot>lisp file, Up: Lisp files [Contents][Index]
snark-deque (system)
src/deque2.lisp
Next: The snark-sparse-array/sparse-array<dot>lisp file, Previous: The snark-deque/deque2<dot>lisp file, Up: Lisp files [Contents][Index]
snark-sparse-array (system)
src/sparse-vector5.lisp
Next: The snark-sparse-array/sparse-vector-expression<dot>lisp file, Previous: The snark-sparse-array/sparse-vector5<dot>lisp file, Up: Lisp files [Contents][Index]
sparse-vector5.lisp (file)
snark-sparse-array (system)
src/sparse-array.lisp
Next: The snark-feature/feature<dot>lisp file, Previous: The snark-sparse-array/sparse-array<dot>lisp file, Up: Lisp files [Contents][Index]
sparse-array.lisp (file)
snark-sparse-array (system)
src/sparse-vector-expression.lisp
Next: The snark-infix-reader/infix-operators<dot>lisp file, Previous: The snark-sparse-array/sparse-vector-expression<dot>lisp file, Up: Lisp files [Contents][Index]
snark-feature (system)
src/feature.lisp
Next: The snark-infix-reader/infix-reader<dot>lisp file, Previous: The snark-feature/feature<dot>lisp file, Up: Lisp files [Contents][Index]
snark-infix-reader (system)
src/infix-operators.lisp
Next: The snark-pkg/snark-pkg<dot>lisp file, Previous: The snark-infix-reader/infix-operators<dot>lisp file, Up: Lisp files [Contents][Index]
infix-operators.lisp (file)
snark-infix-reader (system)
src/infix-reader.lisp
Next: The snark-dpll/davis-putnam3<dot>lisp file, Previous: The snark-infix-reader/infix-reader<dot>lisp file, Up: Lisp files [Contents][Index]
snark-pkg (system)
src/snark-pkg.lisp
Next: The snark-lisp/mvlet<dot>lisp file, Previous: The snark-pkg/snark-pkg<dot>lisp file, Up: Lisp files [Contents][Index]
snark-dpll (system)
src/davis-putnam3.lisp
Next: The snark-lisp/progc<dot>lisp file, Previous: The snark-dpll/davis-putnam3<dot>lisp file, Up: Lisp files [Contents][Index]
snark-lisp (system)
src/mvlet.lisp
Next: The snark-lisp/lisp<dot>lisp file, Previous: The snark-lisp/mvlet<dot>lisp file, Up: Lisp files [Contents][Index]
mvlet.lisp (file)
snark-lisp (system)
src/progc.lisp
Next: The snark-lisp/collectors<dot>lisp file, Previous: The snark-lisp/progc<dot>lisp file, Up: Lisp files [Contents][Index]
progc.lisp (file)
snark-lisp (system)
src/lisp.lisp
Next: The snark-lisp/map-file<dot>lisp file, Previous: The snark-lisp/lisp<dot>lisp file, Up: Lisp files [Contents][Index]
lisp.lisp (file)
snark-lisp (system)
src/collectors.lisp
Next: The snark-lisp/clocks<dot>lisp file, Previous: The snark-lisp/collectors<dot>lisp file, Up: Lisp files [Contents][Index]
collectors.lisp (file)
snark-lisp (system)
src/map-file.lisp
mapnconc-stream0 (function)
Next: The snark-lisp/counters<dot>lisp file, Previous: The snark-lisp/map-file<dot>lisp file, Up: Lisp files [Contents][Index]
map-file.lisp (file)
snark-lisp (system)
src/clocks.lisp
Next: The snark-lisp/pattern-match<dot>lisp file, Previous: The snark-lisp/clocks<dot>lisp file, Up: Lisp files [Contents][Index]
clocks.lisp (file)