The snark Reference Manual

Table of Contents

The snark Reference Manual

This is the snark Reference Manual, generated automatically by Declt version 3.0 "Montgomery Scott" on Wed Oct 13 12:34:29 2021 GMT+0.

1 Introduction

=====
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)
#
#
#
#
#
#
#
#
#
#
#
#
#
#
*

2 Systems

The main system appears first, followed by any subsystem dependency.

2.1 snark

Author

Mark E. Stickel, SRI International

License

MPL 1.1, see file LICENSE

Description

The Snark Theorem Prover

Dependency

snark-implementation (system)

Source

snark.asd (file)

2.2 snark-implementation

Author

Mark E. Stickel, SRI International

License

MPL 1.1, see file LICENSE

Description

The Snark Theorem Prover

Dependencies

• snark-auxiliary-packages (system)
• snark-lisp (system)
• snark-sparse-array (system)
• snark-numbering (system)
• snark-deque (system)
• snark-agenda (system)
• snark-dpll (system)
• snark-feature (system)
• snark-infix-reader (system)
• snark-pkg (system)

Source

snark-implementation.asd (file)

Components

• useful.lisp (file)
• posets.lisp (file)
• solve-sum.lisp (file)
• globals.lisp (file)
• options.lisp (file)
• terms2.lisp (file)
• rows.lisp (file)
• row-contexts.lisp (file)
• constants.lisp (file)
• functions.lisp (file)
• variables.lisp (file)
• subst.lisp (file)
• substitute.lisp (file)
• symbol-table2.lisp (file)
• symbol-definitions.lisp (file)
• assertion-analysis.lisp (file)
• jepd-relations-tables.lisp (file)
• jepd-relations.lisp (file)
• date-reasoning2.lisp (file)
• constraints.lisp (file)
• constraint-purify.lisp (file)
• connectives.lisp (file)
• wffs.lisp (file)
• nonhorn-magic-set.lisp (file)
• dp-refute.lisp (file)
• sorts-functions.lisp (file)
• sorts-interface.lisp (file)
• sorts.lisp (file)
• argument-bag-ac.lisp (file)
• argument-list-a1.lisp (file)
• unify.lisp (file)
• unify-bag.lisp (file)
• subsume-bag.lisp (file)
• unify-vector.lisp (file)
• equal.lisp (file)
• variant.lisp (file)
• alists.lisp (file)
• term-hash.lisp (file)
• trie-index.lisp (file)
• path-index.lisp (file)
• trie.lisp (file)
• feature-vector.lisp (file)
• feature-vector-trie.lisp (file)
• feature-vector-index.lisp (file)
• term-memory.lisp (file)
• weight.lisp (file)
• eval.lisp (file)
• input.lisp (file)
• output.lisp (file)
• simplification-ordering.lisp (file)
• symbol-ordering.lisp (file)
• multiset-ordering.lisp (file)
• recursive-path-ordering.lisp (file)
• ac-rpo.lisp (file)
• knuth-bendix-ordering2.lisp (file)
• rewrite.lisp (file)
• rewrite-code.lisp (file)
• code-for-strings2.lisp (file)
• code-for-numbers3.lisp (file)
• code-for-lists2.lisp (file)
• code-for-bags4.lisp (file)
• resolve-code.lisp (file)
• resolve-code-tables.lisp (file)
• main.lisp (file)
• subsume.lisp (file)
• subsume-clause.lisp (file)
• interactive.lisp (file)
• assertion-file.lisp (file)
• tptp.lisp (file)
• tptp-symbols.lisp (file)
• coder.lisp (file)

2.3 snark-numbering

Author

Mark E. Stickel, SRI International

License

MPL 1.1, see file LICENSE

Description

The Snark Theorem Prover

Dependencies

• snark-auxiliary-packages (system)
• snark-lisp (system)
• snark-sparse-array (system)

Source

snark-numbering.asd (file)

Component

numbering.lisp (file)

2.4 snark-agenda

Author

Mark E. Stickel, SRI International

License

MPL 1.1, see file LICENSE

Description

The Snark Theorem Prover

Dependencies

• snark-auxiliary-packages (system)
• snark-lisp (system)
• snark-deque (system)
• snark-sparse-array (system)

Source

snark-agenda.asd (file)

Component

agenda.lisp (file)

2.5 snark-deque

Author

Mark E. Stickel, SRI International

License

MPL 1.1, see file LICENSE

Description

The Snark Theorem Prover

Dependencies

• snark-auxiliary-packages (system)
• snark-lisp (system)

Source

snark-deque.asd (file)

Component

deque2.lisp (file)

2.6 snark-sparse-array

Author

Mark E. Stickel, SRI International

License

MPL 1.1, see file LICENSE

Description

The Snark Theorem Prover

Dependencies

• snark-auxiliary-packages (system)
• snark-lisp (system)

Source

snark-sparse-array.asd (file)

Components

• sparse-vector5.lisp (file)
• sparse-array.lisp (file)
• sparse-vector-expression.lisp (file)

2.7 snark-feature

Author

Mark E. Stickel, SRI International

License

MPL 1.1, see file LICENSE

Description

The Snark Theorem Prover

Dependencies

• snark-auxiliary-packages (system)
• snark-lisp (system)

Source

snark-feature.asd (file)

Component

feature.lisp (file)

2.8 snark-infix-reader

Author

Mark E. Stickel, SRI International

License

MPL 1.1, see file LICENSE

Description

The Snark Theorem Prover

Dependencies

• snark-auxiliary-packages (system)
• snark-lisp (system)

Source

snark-infix-reader.asd (file)

Components

• infix-operators.lisp (file)
• infix-reader.lisp (file)

2.9 snark-pkg

Author

Mark E. Stickel, SRI International

License

MPL 1.1, see file LICENSE

Description

The Snark Theorem Prover

Dependency

snark-dpll (system)

Source

snark-pkg.asd (file)

Component

snark-pkg.lisp (file)

2.10 snark-dpll

Author

Mark E. Stickel, SRI International

License

MPL 1.1, see file LICENSE

Description

The Snark Theorem Prover

Dependencies

• snark-auxiliary-packages (system)
• snark-lisp (system)

Source

snark-dpll.asd (file)

Component

davis-putnam3.lisp (file)

2.11 snark-lisp

Author

Mark E. Stickel, SRI International

License

MPL 1.1, see file LICENSE

Description

The Snark Theorem Prover

Dependency

snark-auxiliary-packages (system)

Source

snark-lisp.asd (file)

Components

• mvlet.lisp (file)
• progc.lisp (file)
• lisp.lisp (file)
• collectors.lisp (file)
• map-file.lisp (file)
• clocks.lisp (file)
• counters.lisp (file)
• pattern-match.lisp (file)
• topological-sort.lisp (file)

2.12 snark-auxiliary-packages

Author

Mark E. Stickel, SRI International

License

MPL 1.1, see file LICENSE

Description

The Snark Theorem Prover

Source

snark-auxiliary-packages.asd (file)

Component

auxiliary-packages.lisp (file)

3 Files

Files are sorted by type and then listed depth-first from the systems components trees.

3.1 Lisp

3.1.1 snark.asd

Location

snark.asd

Systems

snark (system)

3.1.2 snark-implementation.asd

Location

snark-implementation.asd

Systems

snark-implementation (system)

3.1.3 snark-numbering.asd

Location

snark-numbering.asd

Systems

snark-numbering (system)

3.1.4 snark-agenda.asd

Location

snark-agenda.asd

Systems

snark-agenda (system)

3.1.5 snark-deque.asd

Location

snark-deque.asd

Systems

snark-deque (system)

3.1.6 snark-sparse-array.asd

Location

snark-sparse-array.asd

Systems

snark-sparse-array (system)

3.1.7 snark-feature.asd

Location

snark-feature.asd

Systems

snark-feature (system)

3.1.8 snark-infix-reader.asd

Location

snark-infix-reader.asd

Systems

snark-infix-reader (system)

3.1.9 snark-pkg.asd

Location

snark-pkg.asd

Systems

snark-pkg (system)

3.1.10 snark-dpll.asd

Location

snark-dpll.asd

Systems

snark-dpll (system)

3.1.11 snark-lisp.asd

Location

snark-lisp.asd

Systems

snark-lisp (system)

3.1.12 snark-auxiliary-packages.asd

Location

snark-auxiliary-packages.asd

Systems

snark-auxiliary-packages (system)

3.1.13 snark-implementation/useful.lisp

Parent

snark-implementation (system)

Location

src/useful.lisp

Exported Definitions

• *hash-dollar-package* (special variable)
• *hash-dollar-readtable* (special variable)
• hash-dollar-prin1 (function)
• hash-dollar-print (function)

Internal Definitions

• *outputting-comment* (special variable)
• *terpri-indent* (special variable)
• assoc/eq (compiler macro)
• assoc/eq (function)
• comment (function)
• comment* (compiler macro)
• comment* (function)
• hash-dollar (structure)
• hash-dollar-p (function)
• hash-dollar-reader (function)
• hash-dollar-symbol (function)
• hash-dollar-symbolize (function)
• initialize-hash-dollar-reader (function)
• list-p (function)
• make-hash-dollar (function)
• nocomment (function)
• nocomment* (compiler macro)
• nocomment* (function)
• print-hash-dollar-symbol3 (function)
• setq-once (macro)
• terpri (function)
• terpri-comment (function)
• terpri-comment-indent (function)
• terpri-indent (function)
• unimplemented (function)

3.1.14 snark-implementation/posets.lisp

Dependency

useful.lisp (file)

Parent

snark-implementation (system)

Location

src/posets.lisp

Internal Definitions

• add-edge-transitively (function)
• declare-poset-greaterp (function)
• declare-poset-lessp (function)
• make-poset (function)
• poset-equivalent (function)
• poset-greaterp (compiler macro)
• poset-greaterp (function)
• poset-inferiors (function)
• poset-lessp (compiler macro)
• poset-lessp (function)
• poset-superiors (function)

3.1.15 snark-implementation/solve-sum.lisp

Dependency

posets.lisp (file)

Parent

snark-implementation (system)

Location

src/solve-sum.lisp

Internal Definitions

• solve-sum (function)
• solve-sum-p (function)
• solve-sum-solutions (function)

3.1.16 snark-implementation/globals.lisp

Dependency

solve-sum.lisp (file)

Parent

snark-implementation (system)

Location

src/globals.lisp

Exported Definitions

• resume-snark (function)
• suspend-and-resume-snark (function)
• suspend-snark (function)

Internal Definitions

• *snark-globals* (special variable)
• *snark-nonsave-globals* (special variable)
• audit-snark-globals (function)
• suspend-snark* (function)

3.1.17 snark-implementation/options.lisp

Dependency

globals.lisp (file)

Parent

snark-implementation (system)

Location

src/options.lisp

Exported Definitions

• 1-ary-functions>2-ary-functions-in-default-ordering (generic function)
• 1-ary-functions>2-ary-functions-in-default-ordering (method)
• 1-ary-functions>2-ary-functions-in-default-ordering? (compiler macro)
• 1-ary-functions>2-ary-functions-in-default-ordering? (function)
• agenda-length-before-simplification-limit (generic function)
• agenda-length-before-simplification-limit (method)
• agenda-length-before-simplification-limit (method)
• agenda-length-before-simplification-limit? (compiler macro)
• agenda-length-before-simplification-limit? (function)
• agenda-length-limit (generic function)
• agenda-length-limit (method)
• agenda-length-limit (method)
• agenda-length-limit? (compiler macro)
• agenda-length-limit? (function)
• agenda-ordering-function (generic function)
• agenda-ordering-function (method)
• agenda-ordering-function? (compiler macro)
• agenda-ordering-function? (function)
• allow-skolem-symbols-in-answers (generic function)
• allow-skolem-symbols-in-answers (method)
• allow-skolem-symbols-in-answers? (compiler macro)
• allow-skolem-symbols-in-answers? (function)
• assert-context (generic function)
• assert-context (method)
• assert-context? (compiler macro)
• assert-context? (function)
• assert-sequential (generic function)
• assert-sequential (method)
• assert-sequential? (compiler macro)
• assert-sequential? (function)
• assert-supported (generic function)
• assert-supported (method)
• assert-supported? (compiler macro)
• assert-supported? (function)
• assume-sequential (generic function)
• assume-sequential (method)
• assume-sequential? (compiler macro)
• assume-sequential? (function)
• assume-supported (generic function)
• assume-supported (method)
• assume-supported? (compiler macro)
• assume-supported? (function)
• bag-weight-factorial (generic function)
• bag-weight-factorial (method)
• bag-weight-factorial? (compiler macro)
• bag-weight-factorial? (function)
• builtin-constant-weight (generic function)
• builtin-constant-weight (method)
• builtin-constant-weight? (compiler macro)
• builtin-constant-weight? (function)
• changeable-properties-of-locked-constant (generic function)
• changeable-properties-of-locked-constant (method)
• changeable-properties-of-locked-constant? (compiler macro)
• changeable-properties-of-locked-constant? (function)
• changeable-properties-of-locked-function (generic function)
• changeable-properties-of-locked-function (method)
• changeable-properties-of-locked-function? (compiler macro)
• changeable-properties-of-locked-function? (function)
• declare-root-sort (generic function)
• declare-root-sort (method)
• declare-root-sort? (compiler macro)
• declare-root-sort? (function)
• declare-snark-option (macro)
• declare-string-sort (generic function)
• declare-string-sort (method)
• declare-string-sort? (compiler macro)
• declare-string-sort? (function)
• default-1-ary-functions>2-ary-functions-in-default-ordering (function)
• default-1-ary-functions>2-ary-functions-in-default-ordering? (function)
• default-agenda-length-before-simplification-limit (function)
• default-agenda-length-before-simplification-limit? (function)
• default-agenda-length-limit (function)
• default-agenda-length-limit? (function)
• default-agenda-ordering-function (function)
• default-agenda-ordering-function? (function)
• default-allow-skolem-symbols-in-answers (function)
• default-allow-skolem-symbols-in-answers? (function)
• default-assert-context (function)
• default-assert-context? (function)
• default-assert-sequential (function)
• default-assert-sequential? (function)
• default-assert-supported (function)
• default-assert-supported? (function)
• default-assume-sequential (function)
• default-assume-sequential? (function)
• default-assume-supported (function)
• default-assume-supported? (function)
• default-bag-weight-factorial (function)
• default-bag-weight-factorial? (function)
• default-builtin-constant-weight (function)
• default-builtin-constant-weight? (function)
• default-changeable-properties-of-locked-constant (function)
• default-changeable-properties-of-locked-constant? (function)
• default-changeable-properties-of-locked-function (function)
• default-changeable-properties-of-locked-function? (function)
• default-declare-root-sort (function)
• default-declare-root-sort? (function)
• default-declare-string-sort (function)
• default-declare-string-sort? (function)
• default-input-floats-as-ratios (function)
• default-input-floats-as-ratios? (function)
• default-kbo-builtin-constant-weight (function)
• default-kbo-builtin-constant-weight? (function)
• default-kbo-status (function)
• default-kbo-status? (function)
• default-kbo-variable-weight (function)
• default-kbo-variable-weight? (function)
• default-level-pref-for-giving (function)
• default-level-pref-for-giving? (function)
• default-listen-for-commands (function)
• default-listen-for-commands? (function)
• default-meter-unify-bag (function)
• default-meter-unify-bag? (function)
• default-number-of-given-rows-limit (function)
• default-number-of-given-rows-limit? (function)
• default-number-of-rows-limit (function)
• default-number-of-rows-limit? (function)
• default-ordering-functions>constants (function)
• default-ordering-functions>constants? (function)
• default-partition-communication-table (function)
• default-partition-communication-table? (function)
• default-print-agenda-when-finished (function)
• default-print-agenda-when-finished? (function)
• default-print-assertion-analysis-notes (function)
• default-print-assertion-analysis-notes? (function)
• default-print-clocks-when-finished (function)
• default-print-clocks-when-finished? (function)
• default-print-final-rows (function)
• default-print-final-rows? (function)
• default-print-given-row-lines-printing (function)
• default-print-given-row-lines-printing? (function)
• default-print-given-row-lines-signalling (function)
• default-print-given-row-lines-signalling? (function)
• default-print-irrelevant-rows (function)
• default-print-irrelevant-rows? (function)
• default-print-options-when-starting (function)
• default-print-options-when-starting? (function)
• default-print-pure-rows (function)
• default-print-pure-rows? (function)
• default-print-rewrite-orientation (function)
• default-print-rewrite-orientation? (function)
• default-print-row-answers (function)
• default-print-row-answers? (function)
• default-print-row-constraints (function)
• default-print-row-constraints? (function)
• default-print-row-goals (function)
• default-print-row-goals? (function)
• default-print-row-length-limit (function)
• default-print-row-length-limit? (function)
• default-print-row-partitions (function)
• default-print-row-partitions? (function)
• default-print-row-reasons (function)
• default-print-row-reasons? (function)
• default-print-row-wffs-prettily (function)
• default-print-row-wffs-prettily? (function)
• default-print-rows-prettily (function)
• default-print-rows-prettily? (function)
• default-print-rows-shortened (function)
• default-print-rows-shortened? (function)
• default-print-rows-test (function)
• default-print-rows-test? (function)
• default-print-rows-when-derived (function)
• default-print-rows-when-derived? (function)
• default-print-rows-when-finished (function)
• default-print-rows-when-finished? (function)
• default-print-rows-when-given (function)
• default-print-rows-when-given? (function)
• default-print-rows-when-processed (function)
• default-print-rows-when-processed? (function)
• default-print-summary-when-finished (function)
• default-print-summary-when-finished? (function)
• default-print-symbol-table-warnings (function)
• default-print-symbol-table-warnings? (function)
• default-print-term-memory-when-finished (function)
• default-print-term-memory-when-finished? (function)
• default-print-time-used (function)
• default-print-time-used? (function)
• default-print-unorientable-rows (function)
• default-print-unorientable-rows? (function)
• default-prove-closure (function)
• default-prove-closure? (function)
• default-prove-sequential (function)
• default-prove-sequential? (function)
• default-prove-supported (function)
• default-prove-supported? (function)
• default-pruning-tests (function)
• default-pruning-tests-before-simplification (function)
• default-pruning-tests-before-simplification? (function)
• default-pruning-tests? (function)
• default-rewrite-answers (function)
• default-rewrite-answers? (function)
• default-rewrite-constraints (function)
• default-rewrite-constraints? (function)
• default-row-argument-count-limit (function)
• default-row-argument-count-limit? (function)
• default-row-priority-depth-factor (function)
• default-row-priority-depth-factor? (function)
• default-row-priority-level-factor (function)
• default-row-priority-level-factor? (function)
• default-row-priority-size-factor (function)
• default-row-priority-size-factor? (function)
• default-row-priority-weight-factor (function)
• default-row-priority-weight-factor? (function)
• default-row-weight-before-simplification-limit (function)
• default-row-weight-before-simplification-limit? (function)
• default-row-weight-limit (function)
• default-row-weight-limit? (function)
• default-rpo-status (function)
• default-rpo-status? (function)
• default-run-time-limit (function)
• default-run-time-limit? (function)
• default-test-option14 (function)
• default-test-option14? (function)
• default-test-option17 (function)
• default-test-option17? (function)
• default-test-option18 (function)
• default-test-option18? (function)
• default-test-option19 (function)
• default-test-option19? (function)
• default-test-option2 (function)
• default-test-option20 (function)
• default-test-option20? (function)
• default-test-option21 (function)
• default-test-option21? (function)
• default-test-option23 (function)
• default-test-option23? (function)
• default-test-option29 (function)
• default-test-option29? (function)
• default-test-option2? (function)
• default-test-option3 (function)
• default-test-option30 (function)
• default-test-option30? (function)
• default-test-option36 (function)
• default-test-option36? (function)
• default-test-option37 (function)
• default-test-option37? (function)
• default-test-option38 (function)
• default-test-option38? (function)
• default-test-option39 (function)
• default-test-option39? (function)
• default-test-option3? (function)
• default-test-option40 (function)
• default-test-option40? (function)
• default-test-option41 (function)
• default-test-option41? (function)
• default-test-option42 (function)
• default-test-option42? (function)
• default-test-option43 (function)
• default-test-option43? (function)
• default-test-option44 (function)
• default-test-option44? (function)
• default-test-option45 (function)
• default-test-option45? (function)
• default-test-option49 (function)
• default-test-option49? (function)
• default-test-option50 (function)
• default-test-option50? (function)
• default-test-option51 (function)
• default-test-option51? (function)
• default-test-option52 (function)
• default-test-option52? (function)
• default-test-option53 (function)
• default-test-option53? (function)
• default-test-option54 (function)
• default-test-option54? (function)
• default-test-option55 (function)
• default-test-option55? (function)
• default-test-option56 (function)
• default-test-option56? (function)
• default-test-option57 (function)
• default-test-option57? (function)
• default-test-option58 (function)
• default-test-option58? (function)
• default-test-option59 (function)
• default-test-option59? (function)
• default-test-option6 (function)
• default-test-option60 (function)
• default-test-option60? (function)
• default-test-option6? (function)
• default-test-option8 (function)
• default-test-option8? (function)
• default-test-option9 (function)
• default-test-option9? (function)
• default-trace-dp-refute (function)
• default-trace-dp-refute? (function)
• default-trace-dpll-subsumption (function)
• default-trace-dpll-subsumption? (function)
• default-trace-optimize-sparse-vector-expression (function)
• default-trace-optimize-sparse-vector-expression? (function)
• default-trace-rewrite (function)
• default-trace-rewrite? (function)
• default-trace-unify (function)
• default-trace-unify-bag-basis (function)
• default-trace-unify-bag-basis? (function)
• default-trace-unify-bag-bindings (function)
• default-trace-unify-bag-bindings? (function)
• default-trace-unify? (function)
• default-unify-bag-basis-size-limit (function)
• default-unify-bag-basis-size-limit? (function)
• default-use-ac-connectives (function)
• default-use-ac-connectives? (function)
• default-use-answers-during-subsumption (function)
• default-use-answers-during-subsumption? (function)
• default-use-assertion-analysis (function)
• default-use-assertion-analysis? (function)
• default-use-associative-identity (function)
• default-use-associative-identity? (function)
• default-use-associative-unification (function)
• default-use-associative-unification? (function)
• default-use-clausification (function)
• default-use-clausification? (function)
• default-use-closure-when-satisfiable (function)
• default-use-closure-when-satisfiable? (function)
• default-use-condensing (function)
• default-use-condensing? (function)
• default-use-conditional-answer-creation (function)
• default-use-conditional-answer-creation? (function)
• default-use-constraint-purification (function)
• default-use-constraint-purification? (function)
• default-use-constraint-solver-in-subsumption (function)
• default-use-constraint-solver-in-subsumption? (function)
• default-use-constructive-answer-restriction (function)
• default-use-constructive-answer-restriction? (function)
• default-use-default-ordering (function)
• default-use-default-ordering? (function)
• default-use-dp-subsumption (function)
• default-use-dp-subsumption? (function)
• default-use-embedded-rewrites (function)
• default-use-embedded-rewrites? (function)
• default-use-equality-elimination (function)
• default-use-equality-elimination? (function)
• default-use-equality-factoring (function)
• default-use-equality-factoring? (function)
• default-use-extended-implications (function)
• default-use-extended-implications? (function)
• default-use-extended-quantifiers (function)
• default-use-extended-quantifiers? (function)
• default-use-factoring (function)
• default-use-factoring? (function)
• default-use-function-creation (function)
• default-use-function-creation? (function)
• default-use-hyperresolution (function)
• default-use-hyperresolution? (function)
• default-use-indefinite-answers (function)
• default-use-indefinite-answers? (function)
• default-use-input-restriction (function)
• default-use-input-restriction? (function)
• default-use-literal-ordering-with-hyperresolution (function)
• default-use-literal-ordering-with-hyperresolution? (function)
• default-use-literal-ordering-with-negative-hyperresolution (function)
• default-use-literal-ordering-with-negative-hyperresolution? (function)
• default-use-literal-ordering-with-paramodulation (function)
• default-use-literal-ordering-with-paramodulation? (function)
• default-use-literal-ordering-with-resolution (function)
• default-use-literal-ordering-with-resolution? (function)
• default-use-literal-ordering-with-ur-resolution (function)
• default-use-literal-ordering-with-ur-resolution? (function)
• default-use-lookahead-in-dpll-for-subsumption (function)
• default-use-lookahead-in-dpll-for-subsumption? (function)
• default-use-magic-transformation (function)
• default-use-magic-transformation? (function)
• default-use-negative-hyperresolution (function)
• default-use-negative-hyperresolution? (function)
• default-use-paramodulation (function)
• default-use-paramodulation-only-from-units (function)
• default-use-paramodulation-only-from-units? (function)
• default-use-paramodulation-only-into-units (function)
• default-use-paramodulation-only-into-units? (function)
• default-use-paramodulation? (function)
• default-use-partitions (function)
• default-use-partitions? (function)
• default-use-purity-test (function)
• default-use-purity-test? (function)
• default-use-quantifier-preservation (function)
• default-use-quantifier-preservation? (function)
• default-use-relevance-test (function)
• default-use-relevance-test? (function)
• default-use-replacement-resolution-with-x=x (function)
• default-use-replacement-resolution-with-x=x? (function)
• default-use-resolution (function)
• default-use-resolution? (function)
• default-use-resolve-code (function)
• default-use-resolve-code? (function)
• default-use-simplification-by-equalities (function)
• default-use-simplification-by-equalities? (function)
• default-use-simplification-by-units (function)
• default-use-simplification-by-units? (function)
• default-use-single-replacement-paramodulation (function)
• default-use-single-replacement-paramodulation? (function)
• default-use-sort-relativization (function)
• default-use-sort-relativization? (function)
• default-use-subsumption (function)
• default-use-subsumption-by-false (function)
• default-use-subsumption-by-false? (function)
• default-use-subsumption? (function)
• default-use-term-memory-deletion (function)
• default-use-term-memory-deletion? (function)
• default-use-term-ordering (function)
• default-use-term-ordering-cache (function)
• default-use-term-ordering-cache? (function)
• default-use-term-ordering? (function)
• default-use-to-lisp-code (function)
• default-use-to-lisp-code? (function)
• default-use-unit-restriction (function)
• default-use-unit-restriction? (function)
• default-use-ur-pttp (function)
• default-use-ur-pttp? (function)
• default-use-ur-resolution (function)
• default-use-ur-resolution? (function)
• default-use-variable-name-sorts (function)
• default-use-variable-name-sorts? (function)
• default-use-well-sorting (function)
• default-use-well-sorting? (function)
• default-variable-sort-marker (function)
• default-variable-sort-marker? (function)
• default-variable-symbol-prefixes (function)
• default-variable-symbol-prefixes? (function)
• default-variable-to-lisp-code (function)
• default-variable-to-lisp-code? (function)
• default-variable-weight (function)
• default-variable-weight? (function)
• input-floats-as-ratios (generic function)
• input-floats-as-ratios (method)
• input-floats-as-ratios? (compiler macro)
• input-floats-as-ratios? (function)
• kbo-builtin-constant-weight (generic function)
• kbo-builtin-constant-weight (method)
• kbo-builtin-constant-weight? (compiler macro)
• kbo-builtin-constant-weight? (function)
• kbo-status (generic function)
• kbo-status (method)
• kbo-status? (compiler macro)
• kbo-status? (function)
• kbo-variable-weight (generic function)
• kbo-variable-weight (method)
• kbo-variable-weight? (compiler macro)
• kbo-variable-weight? (function)
• let-options (macro)
• level-pref-for-giving (generic function)
• level-pref-for-giving (method)
• level-pref-for-giving? (compiler macro)
• level-pref-for-giving? (function)
• listen-for-commands (generic function)
• listen-for-commands (method)
• listen-for-commands? (compiler macro)
• listen-for-commands? (function)
• meter-unify-bag (generic function)
• meter-unify-bag (method)
• meter-unify-bag? (compiler macro)
• meter-unify-bag? (function)
• number-of-given-rows-limit (generic function)
• number-of-given-rows-limit (method)
• number-of-given-rows-limit? (compiler macro)
• number-of-given-rows-limit? (function)
• number-of-rows-limit (generic function)
• number-of-rows-limit (method)
• number-of-rows-limit? (compiler macro)
• number-of-rows-limit? (function)
• ordering-functions>constants (generic function)
• ordering-functions>constants (method)
• ordering-functions>constants? (compiler macro)
• ordering-functions>constants? (function)
• partition-communication-table (generic function)
• partition-communication-table (method)
• partition-communication-table? (compiler macro)
• partition-communication-table? (function)
• print-agenda-when-finished (generic function)
• print-agenda-when-finished (method)
• print-agenda-when-finished? (compiler macro)
• print-agenda-when-finished? (function)
• print-assertion-analysis-notes (generic function)
• print-assertion-analysis-notes (method)
• print-assertion-analysis-notes? (compiler macro)
• print-assertion-analysis-notes? (function)
• print-clocks-when-finished (generic function)
• print-clocks-when-finished (method)
• print-clocks-when-finished? (compiler macro)
• print-clocks-when-finished? (function)
• print-final-rows (generic function)
• print-final-rows (method)
• print-final-rows? (compiler macro)
• print-final-rows? (function)
• print-given-row-lines-printing (generic function)
• print-given-row-lines-printing (method)
• print-given-row-lines-printing? (compiler macro)
• print-given-row-lines-printing? (function)
• print-given-row-lines-signalling (generic function)
• print-given-row-lines-signalling (method)
• print-given-row-lines-signalling? (compiler macro)
• print-given-row-lines-signalling? (function)
• print-irrelevant-rows (generic function)
• print-irrelevant-rows (method)
• print-irrelevant-rows? (compiler macro)
• print-irrelevant-rows? (function)
• print-options (function)
• print-options-when-starting (generic function)
• print-options-when-starting (method)
• print-options-when-starting? (compiler macro)
• print-options-when-starting? (function)
• print-pure-rows (generic function)
• print-pure-rows (method)
• print-pure-rows? (compiler macro)
• print-pure-rows? (function)
• print-rewrite-orientation (generic function)
• print-rewrite-orientation (method)
• print-rewrite-orientation? (compiler macro)
• print-rewrite-orientation? (function)
• print-row-answers (generic function)
• print-row-answers (method)
• print-row-answers? (compiler macro)
• print-row-answers? (function)
• print-row-constraints (generic function)
• print-row-constraints (method)
• print-row-constraints? (compiler macro)
• print-row-constraints? (function)
• print-row-goals (generic function)
• print-row-goals (method)
• print-row-goals? (compiler macro)
• print-row-goals? (function)
• print-row-length-limit (generic function)
• print-row-length-limit (method)
• print-row-length-limit? (compiler macro)
• print-row-length-limit? (function)
• print-row-partitions (generic function)
• print-row-partitions (method)
• print-row-partitions? (compiler macro)
• print-row-partitions? (function)
• print-row-reasons (generic function)
• print-row-reasons (method)
• print-row-reasons? (compiler macro)
• print-row-reasons? (function)
• print-row-wffs-prettily (generic function)
• print-row-wffs-prettily (method)
• print-row-wffs-prettily? (compiler macro)
• print-row-wffs-prettily? (function)
• print-rows-prettily (generic function)
• print-rows-prettily (method)
• print-rows-prettily? (compiler macro)
• print-rows-prettily? (function)
• print-rows-shortened (generic function)
• print-rows-shortened (method)
• print-rows-shortened? (compiler macro)
• print-rows-shortened? (function)
• print-rows-test (generic function)
• print-rows-test (method)
• print-rows-test? (compiler macro)
• print-rows-test? (function)
• print-rows-when-derived (generic function)
• print-rows-when-derived (method)
• print-rows-when-derived? (compiler macro)
• print-rows-when-derived? (function)
• print-rows-when-finished (generic function)
• print-rows-when-finished (method)
• print-rows-when-finished? (compiler macro)
• print-rows-when-finished? (function)
• print-rows-when-given (generic function)
• print-rows-when-given (method)
• print-rows-when-given? (compiler macro)
• print-rows-when-given? (function)
• print-rows-when-processed (generic function)
• print-rows-when-processed (method)
• print-rows-when-processed? (compiler macro)
• print-rows-when-processed? (function)
• print-summary-when-finished (generic function)
• print-summary-when-finished (method)
• print-summary-when-finished? (compiler macro)
• print-summary-when-finished? (function)
• print-symbol-table-warnings (generic function)
• print-symbol-table-warnings (method)
• print-symbol-table-warnings? (compiler macro)
• print-symbol-table-warnings? (function)
• print-term-memory-when-finished (generic function)
• print-term-memory-when-finished (method)
• print-term-memory-when-finished? (compiler macro)
• print-term-memory-when-finished? (function)
• print-time-used (generic function)
• print-time-used (method)
• print-time-used? (compiler macro)
• print-time-used? (function)
• print-unorientable-rows (generic function)
• print-unorientable-rows (method)
• print-unorientable-rows? (compiler macro)
• print-unorientable-rows? (function)
• prove-closure (generic function)
• prove-closure (method)
• prove-closure? (compiler macro)
• prove-closure? (function)
• prove-sequential (generic function)
• prove-sequential (method)
• prove-sequential? (compiler macro)
• prove-sequential? (function)
• prove-supported (generic function)
• prove-supported (method)
• prove-supported? (compiler macro)
• prove-supported? (function)
• pruning-tests (generic function)
• pruning-tests (method)
• pruning-tests-before-simplification (generic function)
• pruning-tests-before-simplification (method)
• pruning-tests-before-simplification? (compiler macro)
• pruning-tests-before-simplification? (function)
• pruning-tests? (compiler macro)
• pruning-tests? (function)
• rewrite-answers (generic function)
• rewrite-answers (method)
• rewrite-answers? (compiler macro)
• rewrite-answers? (function)
• rewrite-constraints (generic function)
• rewrite-constraints (method)
• rewrite-constraints? (compiler macro)
• rewrite-constraints? (function)
• row-argument-count-limit (generic function)
• row-argument-count-limit (method)
• row-argument-count-limit? (compiler macro)
• row-argument-count-limit? (function)
• row-priority-depth-factor (generic function)
• row-priority-depth-factor (method)
• row-priority-depth-factor? (compiler macro)
• row-priority-depth-factor? (function)
• row-priority-level-factor (generic function)
• row-priority-level-factor (method)
• row-priority-level-factor? (compiler macro)
• row-priority-level-factor? (function)
• row-priority-size-factor (generic function)
• row-priority-size-factor (method)
• row-priority-size-factor? (compiler macro)
• row-priority-size-factor? (function)
• row-priority-weight-factor (generic function)
• row-priority-weight-factor (method)
• row-priority-weight-factor? (compiler macro)
• row-priority-weight-factor? (function)
• row-weight-before-simplification-limit (generic function)
• row-weight-before-simplification-limit (method)
• row-weight-before-simplification-limit? (compiler macro)
• row-weight-before-simplification-limit? (function)
• row-weight-limit (generic function)
• row-weight-limit (method)
• row-weight-limit? (compiler macro)
• row-weight-limit? (function)
• rpo-status (generic function)
• rpo-status (method)
• rpo-status? (compiler macro)
• rpo-status? (function)
• run-time-limit (generic function)
• run-time-limit (method)
• run-time-limit? (compiler macro)
• run-time-limit? (function)
• set-options (function)
• test-option14 (generic function)
• test-option14 (method)
• test-option14? (compiler macro)
• test-option14? (function)
• test-option17 (generic function)
• test-option17 (method)
• test-option17? (compiler macro)
• test-option17? (function)
• test-option18 (generic function)
• test-option18 (method)
• test-option18? (compiler macro)
• test-option18? (function)
• test-option19 (generic function)
• test-option19 (method)
• test-option19? (compiler macro)
• test-option19? (function)
• test-option2 (generic function)
• test-option2 (method)
• test-option20 (generic function)
• test-option20 (method)
• test-option20? (compiler macro)
• test-option20? (function)
• test-option21 (generic function)
• test-option21 (method)
• test-option21? (compiler macro)
• test-option21? (function)
• test-option23 (generic function)
• test-option23 (method)
• test-option23? (compiler macro)
• test-option23? (function)
• test-option29 (generic function)
• test-option29 (method)
• test-option29? (compiler macro)
• test-option29? (function)
• test-option2? (compiler macro)
• test-option2? (function)
• test-option3 (generic function)
• test-option3 (method)
• test-option30 (generic function)
• test-option30 (method)
• test-option30? (compiler macro)
• test-option30? (function)
• test-option36 (generic function)
• test-option36 (method)
• test-option36? (compiler macro)
• test-option36? (function)
• test-option37 (generic function)
• test-option37 (method)
• test-option37? (compiler macro)
• test-option37? (function)
• test-option38 (generic function)
• test-option38 (method)
• test-option38? (compiler macro)
• test-option38? (function)
• test-option39 (generic function)
• test-option39 (method)
• test-option39? (compiler macro)
• test-option39? (function)
• test-option3? (compiler macro)
• test-option3? (function)
• test-option40 (generic function)
• test-option40 (method)
• test-option40? (compiler macro)
• test-option40? (function)
• test-option41 (generic function)
• test-option41 (method)
• test-option41? (compiler macro)
• test-option41? (function)
• test-option42 (generic function)
• test-option42 (method)
• test-option42? (compiler macro)
• test-option42? (function)
• test-option43 (generic function)
• test-option43 (method)
• test-option43? (compiler macro)
• test-option43? (function)
• test-option44 (generic function)
• test-option44 (method)
• test-option44? (compiler macro)
• test-option44? (function)
• test-option45 (generic function)
• test-option45 (method)
• test-option45? (compiler macro)
• test-option45? (function)
• test-option49 (generic function)
• test-option49 (method)
• test-option49? (compiler macro)
• test-option49? (function)
• test-option50 (generic function)
• test-option50 (method)
• test-option50? (compiler macro)
• test-option50? (function)
• test-option51 (generic function)
• test-option51 (method)
• test-option51? (compiler macro)
• test-option51? (function)
• test-option52 (generic function)
• test-option52 (method)
• test-option52? (compiler macro)
• test-option52? (function)
• test-option53 (generic function)
• test-option53 (method)
• test-option53? (compiler macro)
• test-option53? (function)
• test-option54 (generic function)
• test-option54 (method)
• test-option54? (compiler macro)
• test-option54? (function)
• test-option55 (generic function)
• test-option55 (method)
• test-option55? (compiler macro)
• test-option55? (function)
• test-option56 (generic function)
• test-option56 (method)
• test-option56? (compiler macro)
• test-option56? (function)
• test-option57 (generic function)
• test-option57 (method)
• test-option57? (compiler macro)
• test-option57? (function)
• test-option58 (generic function)
• test-option58 (method)
• test-option58? (compiler macro)
• test-option58? (function)
• test-option59 (generic function)
• test-option59 (method)
• test-option59? (compiler macro)
• test-option59? (function)
• test-option6 (generic function)
• test-option6 (method)
• test-option60 (generic function)
• test-option60 (method)
• test-option60? (compiler macro)
• test-option60? (function)
• test-option6? (compiler macro)
• test-option6? (function)
• test-option8 (generic function)
• test-option8 (method)
• test-option8? (compiler macro)
• test-option8? (function)
• test-option9 (generic function)
• test-option9 (method)
• test-option9? (compiler macro)
• test-option9? (function)
• trace-dp-refute (generic function)
• trace-dp-refute (method)
• trace-dp-refute? (compiler macro)
• trace-dp-refute? (function)
• trace-dpll-subsumption (generic function)
• trace-dpll-subsumption (method)
• trace-dpll-subsumption? (compiler macro)
• trace-dpll-subsumption? (function)
• trace-optimize-sparse-vector-expression (generic function)
• trace-optimize-sparse-vector-expression (method)
• trace-optimize-sparse-vector-expression? (compiler macro)
• trace-optimize-sparse-vector-expression? (function)
• trace-rewrite (generic function)
• trace-rewrite (method)
• trace-rewrite? (compiler macro)
• trace-rewrite? (function)
• trace-unify (generic function)
• trace-unify (method)
• trace-unify-bag-basis (generic function)
• trace-unify-bag-basis (method)
• trace-unify-bag-basis? (compiler macro)
• trace-unify-bag-basis? (function)
• trace-unify-bag-bindings (generic function)
• trace-unify-bag-bindings (method)
• trace-unify-bag-bindings? (compiler macro)
• trace-unify-bag-bindings? (function)
• trace-unify? (compiler macro)
• trace-unify? (function)
• unify-bag-basis-size-limit (generic function)
• unify-bag-basis-size-limit (method)
• unify-bag-basis-size-limit? (compiler macro)
• unify-bag-basis-size-limit? (function)
• use-ac-connectives (generic function)
• use-ac-connectives (method)
• use-ac-connectives? (compiler macro)
• use-ac-connectives? (function)
• use-answers-during-subsumption (generic function)
• use-answers-during-subsumption (method)
• use-answers-during-subsumption? (compiler macro)
• use-answers-during-subsumption? (function)
• use-assertion-analysis (generic function)
• use-assertion-analysis (method)
• use-assertion-analysis? (compiler macro)
• use-assertion-analysis? (function)
• use-associative-identity (generic function)
• use-associative-identity (method)
• use-associative-identity? (compiler macro)
• use-associative-identity? (function)
• use-associative-unification (generic function)
• use-associative-unification (method)
• use-associative-unification? (compiler macro)
• use-associative-unification? (function)
• use-clausification (generic function)
• use-clausification (method)
• use-clausification? (compiler macro)
• use-clausification? (function)
• use-closure-when-satisfiable (generic function)
• use-closure-when-satisfiable (method)
• use-closure-when-satisfiable? (compiler macro)
• use-closure-when-satisfiable? (function)
• use-condensing (generic function)
• use-condensing (method)
• use-condensing? (compiler macro)
• use-condensing? (function)
• use-conditional-answer-creation (generic function)
• use-conditional-answer-creation (method)
• use-conditional-answer-creation? (compiler macro)
• use-conditional-answer-creation? (function)
• use-constraint-purification (generic function)
• use-constraint-purification (method)
• use-constraint-purification (method)
• use-constraint-purification? (compiler macro)
• use-constraint-purification? (function)
• use-constraint-solver-in-subsumption (generic function)
• use-constraint-solver-in-subsumption (method)
• use-constraint-solver-in-subsumption? (compiler macro)
• use-constraint-solver-in-subsumption? (function)
• use-constructive-answer-restriction (generic function)
• use-constructive-answer-restriction (method)
• use-constructive-answer-restriction? (compiler macro)
• use-constructive-answer-restriction? (function)
• use-default-ordering (generic function)
• use-default-ordering (method)
• use-default-ordering? (compiler macro)
• use-default-ordering? (function)
• use-dp-subsumption (generic function)
• use-dp-subsumption (method)
• use-dp-subsumption? (compiler macro)
• use-dp-subsumption? (function)
• use-embedded-rewrites (generic function)
• use-embedded-rewrites (method)
• use-embedded-rewrites? (compiler macro)
• use-embedded-rewrites? (function)
• use-equality-elimination (generic function)
• use-equality-elimination (method)
• use-equality-elimination? (compiler macro)
• use-equality-elimination? (function)
• use-equality-factoring (generic function)
• use-equality-factoring (method)
• use-equality-factoring? (compiler macro)
• use-equality-factoring? (function)
• use-extended-implications (generic function)
• use-extended-implications (method)
• use-extended-implications? (compiler macro)
• use-extended-implications? (function)
• use-extended-quantifiers (generic function)
• use-extended-quantifiers (method)
• use-extended-quantifiers? (compiler macro)
• use-extended-quantifiers? (function)
• use-factoring (generic function)
• use-factoring (method)
• use-factoring? (compiler macro)
• use-factoring? (function)
• use-function-creation (generic function)
• use-function-creation (method)
• use-function-creation? (compiler macro)
• use-function-creation? (function)
• use-hyperresolution (generic function)
• use-hyperresolution (method)
• use-hyperresolution? (compiler macro)
• use-hyperresolution? (function)
• use-indefinite-answers (generic function)
• use-indefinite-answers (method)
• use-indefinite-answers? (compiler macro)
• use-indefinite-answers? (function)
• use-input-restriction (generic function)
• use-input-restriction (method)
• use-input-restriction? (compiler macro)
• use-input-restriction? (function)
• use-literal-ordering-with-hyperresolution (generic function)
• use-literal-ordering-with-hyperresolution (method)
• use-literal-ordering-with-hyperresolution? (compiler macro)
• use-literal-ordering-with-hyperresolution? (function)
• use-literal-ordering-with-negative-hyperresolution (generic function)
• use-literal-ordering-with-negative-hyperresolution (method)
• use-literal-ordering-with-negative-hyperresolution? (compiler macro)
• use-literal-ordering-with-negative-hyperresolution? (function)
• use-literal-ordering-with-paramodulation (generic function)
• use-literal-ordering-with-paramodulation (method)
• use-literal-ordering-with-paramodulation? (compiler macro)
• use-literal-ordering-with-paramodulation? (function)
• use-literal-ordering-with-resolution (generic function)
• use-literal-ordering-with-resolution (method)
• use-literal-ordering-with-resolution? (compiler macro)
• use-literal-ordering-with-resolution? (function)
• use-literal-ordering-with-ur-resolution (generic function)
• use-literal-ordering-with-ur-resolution (method)
• use-literal-ordering-with-ur-resolution? (compiler macro)
• use-literal-ordering-with-ur-resolution? (function)
• use-lookahead-in-dpll-for-subsumption (generic function)
• use-lookahead-in-dpll-for-subsumption (method)
• use-lookahead-in-dpll-for-subsumption? (compiler macro)
• use-lookahead-in-dpll-for-subsumption? (function)
• use-magic-transformation (generic function)
• use-magic-transformation (method)
• use-magic-transformation? (compiler macro)
• use-magic-transformation? (function)
• use-negative-hyperresolution (generic function)
• use-negative-hyperresolution (method)
• use-negative-hyperresolution? (compiler macro)
• use-negative-hyperresolution? (function)
• use-paramodulation (generic function)
• use-paramodulation (method)
• use-paramodulation-only-from-units (generic function)
• use-paramodulation-only-from-units (method)
• use-paramodulation-only-from-units? (compiler macro)
• use-paramodulation-only-from-units? (function)
• use-paramodulation-only-into-units (generic function)
• use-paramodulation-only-into-units (method)
• use-paramodulation-only-into-units? (compiler macro)
• use-paramodulation-only-into-units? (function)
• use-paramodulation? (compiler macro)
• use-paramodulation? (function)
• use-partitions (generic function)
• use-partitions (method)
• use-partitions? (compiler macro)
• use-partitions? (function)
• use-purity-test (generic function)
• use-purity-test (method)
• use-purity-test? (compiler macro)
• use-purity-test? (function)
• use-quantifier-preservation (generic function)
• use-quantifier-preservation (method)
• use-quantifier-preservation? (compiler macro)
• use-quantifier-preservation? (function)
• use-relevance-test (generic function)
• use-relevance-test (method)
• use-relevance-test? (compiler macro)
• use-relevance-test? (function)
• use-replacement-resolution-with-x=x (generic function)
• use-replacement-resolution-with-x=x (method)
• use-replacement-resolution-with-x=x? (compiler macro)
• use-replacement-resolution-with-x=x? (function)
• use-resolution (generic function)
• use-resolution (method)
• use-resolution? (compiler macro)
• use-resolution? (function)
• use-resolve-code (generic function)
• use-resolve-code (method)
• use-resolve-code (method)
• use-resolve-code? (compiler macro)
• use-resolve-code? (function)
• use-simplification-by-equalities (generic function)
• use-simplification-by-equalities (method)
• use-simplification-by-equalities? (compiler macro)
• use-simplification-by-equalities? (function)
• use-simplification-by-units (generic function)
• use-simplification-by-units (method)
• use-simplification-by-units? (compiler macro)
• use-simplification-by-units? (function)
• use-single-replacement-paramodulation (generic function)
• use-single-replacement-paramodulation (method)
• use-single-replacement-paramodulation? (compiler macro)
• use-single-replacement-paramodulation? (function)
• use-sort-relativization (generic function)
• use-sort-relativization (method)
• use-sort-relativization? (compiler macro)
• use-sort-relativization? (function)
• use-subsumption (generic function)
• use-subsumption (method)
• use-subsumption-by-false (generic function)
• use-subsumption-by-false (method)
• use-subsumption-by-false? (compiler macro)
• use-subsumption-by-false? (function)
• use-subsumption? (compiler macro)
• use-subsumption? (function)
• use-term-memory-deletion (generic function)
• use-term-memory-deletion (method)
• use-term-memory-deletion? (compiler macro)
• use-term-memory-deletion? (function)
• use-term-ordering (generic function)
• use-term-ordering (method)
• use-term-ordering (method)
• use-term-ordering-cache (generic function)
• use-term-ordering-cache (method)
• use-term-ordering-cache? (compiler macro)
• use-term-ordering-cache? (function)
• use-term-ordering? (compiler macro)
• use-term-ordering? (function)
• use-to-lisp-code (generic function)
• use-to-lisp-code (method)
• use-to-lisp-code? (compiler macro)
• use-to-lisp-code? (function)
• use-unit-restriction (generic function)
• use-unit-restriction (method)
• use-unit-restriction? (compiler macro)
• use-unit-restriction? (function)
• use-ur-pttp (generic function)
• use-ur-pttp (method)
• use-ur-pttp? (compiler macro)
• use-ur-pttp? (function)
• use-ur-resolution (generic function)
• use-ur-resolution (method)
• use-ur-resolution? (compiler macro)
• use-ur-resolution? (function)
• use-variable-name-sorts (generic function)
• use-variable-name-sorts (method)
• use-variable-name-sorts? (compiler macro)
• use-variable-name-sorts? (function)
• use-well-sorting (generic function)
• use-well-sorting (method)
• use-well-sorting? (compiler macro)
• use-well-sorting? (function)
• variable-sort-marker (generic function)
• variable-sort-marker (method)
• variable-sort-marker? (compiler macro)
• variable-sort-marker? (function)
• variable-symbol-prefixes (generic function)
• variable-symbol-prefixes (method)
• variable-symbol-prefixes? (compiler macro)
• variable-symbol-prefixes? (function)
• variable-to-lisp-code (generic function)
• variable-to-lisp-code (method)
• variable-to-lisp-code? (compiler macro)
• variable-to-lisp-code? (function)
• variable-weight (generic function)
• variable-weight (method)
• variable-weight? (compiler macro)
• variable-weight? (function)

Internal Definitions

• *%1-ary-functions>2-ary-functions-in-default-ordering%* (special variable)
• *%agenda-length-before-simplification-limit%* (special variable)
• *%agenda-length-limit%* (special variable)
• *%agenda-ordering-function%* (special variable)
• *%allow-skolem-symbols-in-answers%* (special variable)
• *%assert-context%* (special variable)
• *%assert-sequential%* (special variable)
• *%assert-supported%* (special variable)
• *%assume-sequential%* (special variable)
• *%assume-supported%* (special variable)
• *%bag-weight-factorial%* (special variable)
• *%builtin-constant-weight%* (special variable)
• *%changeable-properties-of-locked-constant%* (special variable)
• *%changeable-properties-of-locked-function%* (special variable)
• *%declare-root-sort%* (special variable)
• *%declare-string-sort%* (special variable)
• *%default-1-ary-functions>2-ary-functions-in-default-ordering%* (special variable)
• *%default-agenda-length-before-simplification-limit%* (special variable)
• *%default-agenda-length-limit%* (special variable)
• *%default-agenda-ordering-function%* (special variable)
• *%default-allow-skolem-symbols-in-answers%* (special variable)
• *%default-assert-context%* (special variable)
• *%default-assert-sequential%* (special variable)
• *%default-assert-supported%* (special variable)
• *%default-assume-sequential%* (special variable)
• *%default-assume-supported%* (special variable)
• *%default-bag-weight-factorial%* (special variable)
• *%default-builtin-constant-weight%* (special variable)
• *%default-changeable-properties-of-locked-constant%* (special variable)
• *%default-changeable-properties-of-locked-function%* (special variable)
• *%default-declare-root-sort%* (special variable)
• *%default-declare-string-sort%* (special variable)
• *%default-input-floats-as-ratios%* (special variable)
• *%default-kbo-builtin-constant-weight%* (special variable)
• *%default-kbo-status%* (special variable)
• *%default-kbo-variable-weight%* (special variable)
• *%default-level-pref-for-giving%* (special variable)
• *%default-listen-for-commands%* (special variable)
• *%default-meter-unify-bag%* (special variable)
• *%default-number-of-given-rows-limit%* (special variable)
• *%default-number-of-rows-limit%* (special variable)
• *%default-ordering-functions>constants%* (special variable)
• *%default-partition-communication-table%* (special variable)
• *%default-print-agenda-when-finished%* (special variable)
• *%default-print-assertion-analysis-notes%* (special variable)
• *%default-print-clocks-when-finished%* (special variable)
• *%default-print-final-rows%* (special variable)
• *%default-print-given-row-lines-printing%* (special variable)
• *%default-print-given-row-lines-signalling%* (special variable)
• *%default-print-irrelevant-rows%* (special variable)
• *%default-print-options-when-starting%* (special variable)
• *%default-print-pure-rows%* (special variable)
• *%default-print-rewrite-orientation%* (special variable)
• *%default-print-row-answers%* (special variable)
• *%default-print-row-constraints%* (special variable)
• *%default-print-row-goals%* (special variable)
• *%default-print-row-length-limit%* (special variable)
• *%default-print-row-partitions%* (special variable)
• *%default-print-row-reasons%* (special variable)
• *%default-print-row-wffs-prettily%* (special variable)
• *%default-print-rows-prettily%* (special variable)
• *%default-print-rows-shortened%* (special variable)
• *%default-print-rows-test%* (special variable)
• *%default-print-rows-when-derived%* (special variable)
• *%default-print-rows-when-finished%* (special variable)
• *%default-print-rows-when-given%* (special variable)
• *%default-print-rows-when-processed%* (special variable)
• *%default-print-summary-when-finished%* (special variable)
• *%default-print-symbol-table-warnings%* (special variable)
• *%default-print-term-memory-when-finished%* (special variable)
• *%default-print-time-used%* (special variable)
• *%default-print-unorientable-rows%* (special variable)
• *%default-prove-closure%* (special variable)
• *%default-prove-sequential%* (special variable)
• *%default-prove-supported%* (special variable)
• *%default-pruning-tests%* (special variable)
• *%default-pruning-tests-before-simplification%* (special variable)
• *%default-rewrite-answers%* (special variable)
• *%default-rewrite-constraints%* (special variable)
• *%default-row-argument-count-limit%* (special variable)
• *%default-row-priority-depth-factor%* (special variable)
• *%default-row-priority-level-factor%* (special variable)
• *%default-row-priority-size-factor%* (special variable)
• *%default-row-priority-weight-factor%* (special variable)
• *%default-row-weight-before-simplification-limit%* (special variable)
• *%default-row-weight-limit%* (special variable)
• *%default-rpo-status%* (special variable)
• *%default-run-time-limit%* (special variable)
• *%default-test-option14%* (special variable)
• *%default-test-option17%* (special variable)
• *%default-test-option18%* (special variable)
• *%default-test-option19%* (special variable)
• *%default-test-option2%* (special variable)
• *%default-test-option20%* (special variable)
• *%default-test-option21%* (special variable)
• *%default-test-option23%* (special variable)
• *%default-test-option29%* (special variable)
• *%default-test-option3%* (special variable)
• *%default-test-option30%* (special variable)
• *%default-test-option36%* (special variable)
• *%default-test-option37%* (special variable)
• *%default-test-option38%* (special variable)
• *%default-test-option39%* (special variable)
• *%default-test-option40%* (special variable)
• *%default-test-option41%* (special variable)
• *%default-test-option42%* (special variable)
• *%default-test-option43%* (special variable)
• *%default-test-option44%* (special variable)
• *%default-test-option45%* (special variable)
• *%default-test-option49%* (special variable)
• *%default-test-option50%* (special variable)
• *%default-test-option51%* (special variable)
• *%default-test-option52%* (special variable)
• *%default-test-option53%* (special variable)
• *%default-test-option54%* (special variable)
• *%default-test-option55%* (special variable)
• *%default-test-option56%* (special variable)
• *%default-test-option57%* (special variable)
• *%default-test-option58%* (special variable)
• *%default-test-option59%* (special variable)
• *%default-test-option6%* (special variable)
• *%default-test-option60%* (special variable)
• *%default-test-option8%* (special variable)
• *%default-test-option9%* (special variable)
• *%default-trace-dp-refute%* (special variable)
• *%default-trace-dpll-subsumption%* (special variable)
• *%default-trace-optimize-sparse-vector-expression%* (special variable)
• *%default-trace-rewrite%* (special variable)
• *%default-trace-unify%* (special variable)
• *%default-trace-unify-bag-basis%* (special variable)
• *%default-trace-unify-bag-bindings%* (special variable)
• *%default-unify-bag-basis-size-limit%* (special variable)
• *%default-use-ac-connectives%* (special variable)
• *%default-use-answers-during-subsumption%* (special variable)
• *%default-use-assertion-analysis%* (special variable)
• *%default-use-associative-identity%* (special variable)
• *%default-use-associative-unification%* (special variable)
• *%default-use-clausification%* (special variable)
• *%default-use-closure-when-satisfiable%* (special variable)
• *%default-use-condensing%* (special variable)
• *%default-use-conditional-answer-creation%* (special variable)
• *%default-use-constraint-purification%* (special variable)
• *%default-use-constraint-solver-in-subsumption%* (special variable)
• *%default-use-constructive-answer-restriction%* (special variable)
• *%default-use-default-ordering%* (special variable)
• *%default-use-dp-subsumption%* (special variable)
• *%default-use-embedded-rewrites%* (special variable)
• *%default-use-equality-elimination%* (special variable)
• *%default-use-equality-factoring%* (special variable)
• *%default-use-extended-implications%* (special variable)
• *%default-use-extended-quantifiers%* (special variable)
• *%default-use-factoring%* (special variable)
• *%default-use-function-creation%* (special variable)
• *%default-use-hyperresolution%* (special variable)
• *%default-use-indefinite-answers%* (special variable)
• *%default-use-input-restriction%* (special variable)
• *%default-use-literal-ordering-with-hyperresolution%* (special variable)
• *%default-use-literal-ordering-with-negative-hyperresolution%* (special variable)
• *%default-use-literal-ordering-with-paramodulation%* (special variable)
• *%default-use-literal-ordering-with-resolution%* (special variable)
• *%default-use-literal-ordering-with-ur-resolution%* (special variable)
• *%default-use-lookahead-in-dpll-for-subsumption%* (special variable)
• *%default-use-magic-transformation%* (special variable)
• *%default-use-negative-hyperresolution%* (special variable)
• *%default-use-paramodulation%* (special variable)
• *%default-use-paramodulation-only-from-units%* (special variable)
• *%default-use-paramodulation-only-into-units%* (special variable)
• *%default-use-partitions%* (special variable)
• *%default-use-purity-test%* (special variable)
• *%default-use-quantifier-preservation%* (special variable)
• *%default-use-relevance-test%* (special variable)
• *%default-use-replacement-resolution-with-x=x%* (special variable)
• *%default-use-resolution%* (special variable)
• *%default-use-resolve-code%* (special variable)
• *%default-use-simplification-by-equalities%* (special variable)
• *%default-use-simplification-by-units%* (special variable)
• *%default-use-single-replacement-paramodulation%* (special variable)
• *%default-use-sort-relativization%* (special variable)
• *%default-use-subsumption%* (special variable)
• *%default-use-subsumption-by-false%* (special variable)
• *%default-use-term-memory-deletion%* (special variable)
• *%default-use-term-ordering%* (special variable)
• *%default-use-term-ordering-cache%* (special variable)
• *%default-use-to-lisp-code%* (special variable)
• *%default-use-unit-restriction%* (special variable)
• *%default-use-ur-pttp%* (special variable)
• *%default-use-ur-resolution%* (special variable)
• *%default-use-variable-name-sorts%* (special variable)
• *%default-use-well-sorting%* (special variable)
• *%default-variable-sort-marker%* (special variable)
• *%default-variable-symbol-prefixes%* (special variable)
• *%default-variable-to-lisp-code%* (special variable)
• *%default-variable-weight%* (special variable)
• *%input-floats-as-ratios%* (special variable)
• *%invisible-1-ary-functions>2-ary-functions-in-default-ordering%* (special variable)
• *%invisible-agenda-length-before-simplification-limit%* (special variable)
• *%invisible-agenda-length-limit%* (special variable)
• *%invisible-agenda-ordering-function%* (special variable)
• *%invisible-allow-skolem-symbols-in-answers%* (special variable)
• *%invisible-assert-context%* (special variable)
• *%invisible-assert-sequential%* (special variable)
• *%invisible-assert-supported%* (special variable)
• *%invisible-assume-sequential%* (special variable)
• *%invisible-assume-supported%* (special variable)
• *%invisible-bag-weight-factorial%* (special variable)
• *%invisible-builtin-constant-weight%* (special variable)
• *%invisible-changeable-properties-of-locked-constant%* (special variable)
• *%invisible-changeable-properties-of-locked-function%* (special variable)
• *%invisible-declare-root-sort%* (special variable)
• *%invisible-declare-string-sort%* (special variable)
• *%invisible-input-floats-as-ratios%* (special variable)
• *%invisible-kbo-builtin-constant-weight%* (special variable)
• *%invisible-kbo-status%* (special variable)
• *%invisible-kbo-variable-weight%* (special variable)
• *%invisible-level-pref-for-giving%* (special variable)
• *%invisible-listen-for-commands%* (special variable)
• *%invisible-meter-unify-bag%* (special variable)
• *%invisible-number-of-given-rows-limit%* (special variable)
• *%invisible-number-of-rows-limit%* (special variable)
• *%invisible-ordering-functions>constants%* (special variable)
• *%invisible-partition-communication-table%* (special variable)
• *%invisible-print-agenda-when-finished%* (special variable)
• *%invisible-print-assertion-analysis-notes%* (special variable)
• *%invisible-print-clocks-when-finished%* (special variable)
• *%invisible-print-final-rows%* (special variable)
• *%invisible-print-given-row-lines-printing%* (special variable)
• *%invisible-print-given-row-lines-signalling%* (special variable)
• *%invisible-print-irrelevant-rows%* (special variable)
• *%invisible-print-options-when-starting%* (special variable)
• *%invisible-print-pure-rows%* (special variable)
• *%invisible-print-rewrite-orientation%* (special variable)
• *%invisible-print-row-answers%* (special variable)
• *%invisible-print-row-constraints%* (special variable)
• *%invisible-print-row-goals%* (special variable)
• *%invisible-print-row-length-limit%* (special variable)
• *%invisible-print-row-partitions%* (special variable)
• *%invisible-print-row-reasons%* (special variable)
• *%invisible-print-row-wffs-prettily%* (special variable)
• *%invisible-print-rows-prettily%* (special variable)
• *%invisible-print-rows-shortened%* (special variable)
• *%invisible-print-rows-test%* (special variable)
• *%invisible-print-rows-when-derived%* (special variable)
• *%invisible-print-rows-when-finished%* (special variable)
• *%invisible-print-rows-when-given%* (special variable)
• *%invisible-print-rows-when-processed%* (special variable)
• *%invisible-print-summary-when-finished%* (special variable)
• *%invisible-print-symbol-table-warnings%* (special variable)
• *%invisible-print-term-memory-when-finished%* (special variable)
• *%invisible-print-time-used%* (special variable)
• *%invisible-print-unorientable-rows%* (special variable)
• *%invisible-prove-closure%* (special variable)
• *%invisible-prove-sequential%* (special variable)
• *%invisible-prove-supported%* (special variable)
• *%invisible-pruning-tests%* (special variable)
• *%invisible-pruning-tests-before-simplification%* (special variable)
• *%invisible-rewrite-answers%* (special variable)
• *%invisible-rewrite-constraints%* (special variable)
• *%invisible-row-argument-count-limit%* (special variable)
• *%invisible-row-priority-depth-factor%* (special variable)
• *%invisible-row-priority-level-factor%* (special variable)
• *%invisible-row-priority-size-factor%* (special variable)
• *%invisible-row-priority-weight-factor%* (special variable)
• *%invisible-row-weight-before-simplification-limit%* (special variable)
• *%invisible-row-weight-limit%* (special variable)
• *%invisible-rpo-status%* (special variable)
• *%invisible-run-time-limit%* (special variable)
• *%invisible-test-option14%* (special variable)
• *%invisible-test-option17%* (special variable)
• *%invisible-test-option18%* (special variable)
• *%invisible-test-option19%* (special variable)
• *%invisible-test-option2%* (special variable)
• *%invisible-test-option20%* (special variable)
• *%invisible-test-option21%* (special variable)
• *%invisible-test-option23%* (special variable)
• *%invisible-test-option29%* (special variable)
• *%invisible-test-option3%* (special variable)
• *%invisible-test-option30%* (special variable)
• *%invisible-test-option36%* (special variable)
• *%invisible-test-option37%* (special variable)
• *%invisible-test-option38%* (special variable)
• *%invisible-test-option39%* (special variable)
• *%invisible-test-option40%* (special variable)
• *%invisible-test-option41%* (special variable)
• *%invisible-test-option42%* (special variable)
• *%invisible-test-option43%* (special variable)
• *%invisible-test-option44%* (special variable)
• *%invisible-test-option45%* (special variable)
• *%invisible-test-option49%* (special variable)
• *%invisible-test-option50%* (special variable)
• *%invisible-test-option51%* (special variable)
• *%invisible-test-option52%* (special variable)
• *%invisible-test-option53%* (special variable)
• *%invisible-test-option54%* (special variable)
• *%invisible-test-option55%* (special variable)
• *%invisible-test-option56%* (special variable)
• *%invisible-test-option57%* (special variable)
• *%invisible-test-option58%* (special variable)
• *%invisible-test-option59%* (special variable)
• *%invisible-test-option6%* (special variable)
• *%invisible-test-option60%* (special variable)
• *%invisible-test-option8%* (special variable)
• *%invisible-test-option9%* (special variable)
• *%invisible-trace-dp-refute%* (special variable)
• *%invisible-trace-dpll-subsumption%* (special variable)
• *%invisible-trace-optimize-sparse-vector-expression%* (special variable)
• *%invisible-trace-rewrite%* (special variable)
• *%invisible-trace-unify%* (special variable)
• *%invisible-trace-unify-bag-basis%* (special variable)
• *%invisible-trace-unify-bag-bindings%* (special variable)
• *%invisible-unify-bag-basis-size-limit%* (special variable)
• *%invisible-use-ac-connectives%* (special variable)
• *%invisible-use-answers-during-subsumption%* (special variable)
• *%invisible-use-assertion-analysis%* (special variable)
• *%invisible-use-associative-identity%* (special variable)
• *%invisible-use-associative-unification%* (special variable)
• *%invisible-use-clausification%* (special variable)
• *%invisible-use-closure-when-satisfiable%* (special variable)
• *%invisible-use-condensing%* (special variable)
• *%invisible-use-conditional-answer-creation%* (special variable)
• *%invisible-use-constraint-purification%* (special variable)
• *%invisible-use-constraint-solver-in-subsumption%* (special variable)
• *%invisible-use-constructive-answer-restriction%* (special variable)
• *%invisible-use-default-ordering%* (special variable)
• *%invisible-use-dp-subsumption%* (special variable)
• *%invisible-use-embedded-rewrites%* (special variable)
• *%invisible-use-equality-elimination%* (special variable)
• *%invisible-use-equality-factoring%* (special variable)
• *%invisible-use-extended-implications%* (special variable)
• *%invisible-use-extended-quantifiers%* (special variable)
• *%invisible-use-factoring%* (special variable)
• *%invisible-use-function-creation%* (special variable)
• *%invisible-use-hyperresolution%* (special variable)
• *%invisible-use-indefinite-answers%* (special variable)
• *%invisible-use-input-restriction%* (special variable)
• *%invisible-use-literal-ordering-with-hyperresolution%* (special variable)
• *%invisible-use-literal-ordering-with-negative-hyperresolution%* (special variable)
• *%invisible-use-literal-ordering-with-paramodulation%* (special variable)
• *%invisible-use-literal-ordering-with-resolution%* (special variable)
• *%invisible-use-literal-ordering-with-ur-resolution%* (special variable)
• *%invisible-use-lookahead-in-dpll-for-subsumption%* (special variable)
• *%invisible-use-magic-transformation%* (special variable)
• *%invisible-use-negative-hyperresolution%* (special variable)
• *%invisible-use-paramodulation%* (special variable)
• *%invisible-use-paramodulation-only-from-units%* (special variable)
• *%invisible-use-paramodulation-only-into-units%* (special variable)
• *%invisible-use-partitions%* (special variable)
• *%invisible-use-purity-test%* (special variable)
• *%invisible-use-quantifier-preservation%* (special variable)
• *%invisible-use-relevance-test%* (special variable)
• *%invisible-use-replacement-resolution-with-x=x%* (special variable)
• *%invisible-use-resolution%* (special variable)
• *%invisible-use-resolve-code%* (special variable)
• *%invisible-use-simplification-by-equalities%* (special variable)
• *%invisible-use-simplification-by-units%* (special variable)
• *%invisible-use-single-replacement-paramodulation%* (special variable)
• *%invisible-use-sort-relativization%* (special variable)
• *%invisible-use-subsumption%* (special variable)
• *%invisible-use-subsumption-by-false%* (special variable)
• *%invisible-use-term-memory-deletion%* (special variable)
• *%invisible-use-term-ordering%* (special variable)
• *%invisible-use-term-ordering-cache%* (special variable)
• *%invisible-use-to-lisp-code%* (special variable)
• *%invisible-use-unit-restriction%* (special variable)
• *%invisible-use-ur-pttp%* (special variable)
• *%invisible-use-ur-resolution%* (special variable)
• *%invisible-use-variable-name-sorts%* (special variable)
• *%invisible-use-well-sorting%* (special variable)
• *%invisible-variable-sort-marker%* (special variable)
• *%invisible-variable-symbol-prefixes%* (special variable)
• *%invisible-variable-to-lisp-code%* (special variable)
• *%invisible-variable-weight%* (special variable)
• *%kbo-builtin-constant-weight%* (special variable)
• *%kbo-status%* (special variable)
• *%kbo-variable-weight%* (special variable)
• *%level-pref-for-giving%* (special variable)
• *%listen-for-commands%* (special variable)
• *%meter-unify-bag%* (special variable)
• *%number-of-given-rows-limit%* (special variable)
• *%number-of-rows-limit%* (special variable)
• *%ordering-functions>constants%* (special variable)
• *%partition-communication-table%* (special variable)
• *%print-agenda-when-finished%* (special variable)
• *%print-assertion-analysis-notes%* (special variable)
• *%print-clocks-when-finished%* (special variable)
• *%print-final-rows%* (special variable)
• *%print-given-row-lines-printing%* (special variable)
• *%print-given-row-lines-signalling%* (special variable)
• *%print-irrelevant-rows%* (special variable)
• *%print-options-when-starting%* (special variable)
• *%print-pure-rows%* (special variable)
• *%print-rewrite-orientation%* (special variable)
• *%print-row-answers%* (special variable)
• *%print-row-constraints%* (special variable)
• *%print-row-goals%* (special variable)
• *%print-row-length-limit%* (special variable)
• *%print-row-partitions%* (special variable)
• *%print-row-reasons%* (special variable)
• *%print-row-wffs-prettily%* (special variable)
• *%print-rows-prettily%* (special variable)
• *%print-rows-shortened%* (special variable)
• *%print-rows-test%* (special variable)
• *%print-rows-when-derived%* (special variable)
• *%print-rows-when-finished%* (special variable)
• *%print-rows-when-given%* (special variable)
• *%print-rows-when-processed%* (special variable)
• *%print-summary-when-finished%* (special variable)
• *%print-symbol-table-warnings%* (special variable)
• *%print-term-memory-when-finished%* (special variable)
• *%print-time-used%* (special variable)
• *%print-unorientable-rows%* (special variable)
• *%prove-closure%* (special variable)
• *%prove-sequential%* (special variable)
• *%prove-supported%* (special variable)
• *%pruning-tests%* (special variable)
• *%pruning-tests-before-simplification%* (special variable)
• *%rewrite-answers%* (special variable)
• *%rewrite-constraints%* (special variable)
• *%row-argument-count-limit%* (special variable)
• *%row-priority-depth-factor%* (special variable)
• *%row-priority-level-factor%* (special variable)
• *%row-priority-size-factor%* (special variable)
• *%row-priority-weight-factor%* (special variable)
• *%row-weight-before-simplification-limit%* (special variable)
• *%row-weight-limit%* (special variable)
• *%rpo-status%* (special variable)
• *%run-time-limit%* (special variable)
• *%test-option14%* (special variable)
• *%test-option17%* (special variable)
• *%test-option18%* (special variable)
• *%test-option19%* (special variable)
• *%test-option2%* (special variable)
• *%test-option20%* (special variable)
• *%test-option21%* (special variable)
• *%test-option23%* (special variable)
• *%test-option29%* (special variable)
• *%test-option3%* (special variable)
• *%test-option30%* (special variable)
• *%test-option36%* (special variable)
• *%test-option37%* (special variable)
• *%test-option38%* (special variable)
• *%test-option39%* (special variable)
• *%test-option40%* (special variable)
• *%test-option41%* (special variable)
• *%test-option42%* (special variable)
• *%test-option43%* (special variable)
• *%test-option44%* (special variable)
• *%test-option45%* (special variable)
• *%test-option49%* (special variable)
• *%test-option50%* (special variable)
• *%test-option51%* (special variable)
• *%test-option52%* (special variable)
• *%test-option53%* (special variable)
• *%test-option54%* (special variable)
• *%test-option55%* (special variable)
• *%test-option56%* (special variable)
• *%test-option57%* (special variable)
• *%test-option58%* (special variable)
• *%test-option59%* (special variable)
• *%test-option6%* (special variable)
• *%test-option60%* (special variable)
• *%test-option8%* (special variable)
• *%test-option9%* (special variable)
• *%trace-dp-refute%* (special variable)
• *%trace-dpll-subsumption%* (special variable)
• *%trace-optimize-sparse-vector-expression%* (special variable)
• *%trace-rewrite%* (special variable)
• *%trace-unify%* (special variable)
• *%trace-unify-bag-basis%* (special variable)
• *%trace-unify-bag-bindings%* (special variable)
• *%unify-bag-basis-size-limit%* (special variable)
• *%use-ac-connectives%* (special variable)
• *%use-answers-during-subsumption%* (special variable)
• *%use-assertion-analysis%* (special variable)
• *%use-associative-identity%* (special variable)
• *%use-associative-unification%* (special variable)
• *%use-clausification%* (special variable)
• *%use-closure-when-satisfiable%* (special variable)
• *%use-condensing%* (special variable)
• *%use-conditional-answer-creation%* (special variable)
• *%use-constraint-purification%* (special variable)
• *%use-constraint-solver-in-subsumption%* (special variable)
• *%use-constructive-answer-restriction%* (special variable)
• *%use-default-ordering%* (special variable)
• *%use-dp-subsumption%* (special variable)
• *%use-embedded-rewrites%* (special variable)
• *%use-equality-elimination%* (special variable)
• *%use-equality-factoring%* (special variable)
• *%use-extended-implications%* (special variable)
• *%use-extended-quantifiers%* (special variable)
• *%use-factoring%* (special variable)
• *%use-function-creation%* (special variable)
• *%use-hyperresolution%* (special variable)
• *%use-indefinite-answers%* (special variable)
• *%use-input-restriction%* (special variable)
• *%use-literal-ordering-with-hyperresolution%* (special variable)
• *%use-literal-ordering-with-negative-hyperresolution%* (special variable)
• *%use-literal-ordering-with-paramodulation%* (special variable)
• *%use-literal-ordering-with-resolution%* (special variable)
• *%use-literal-ordering-with-ur-resolution%* (special variable)
• *%use-lookahead-in-dpll-for-subsumption%* (special variable)
• *%use-magic-transformation%* (special variable)
• *%use-negative-hyperresolution%* (special variable)
• *%use-paramodulation%* (special variable)
• *%use-paramodulation-only-from-units%* (special variable)
• *%use-paramodulation-only-into-units%* (special variable)
• *%use-partitions%* (special variable)
• *%use-purity-test%* (special variable)
• *%use-quantifier-preservation%* (special variable)
• *%use-relevance-test%* (special variable)
• *%use-replacement-resolution-with-x=x%* (special variable)
• *%use-resolution%* (special variable)
• *%use-resolve-code%* (special variable)
• *%use-simplification-by-equalities%* (special variable)
• *%use-simplification-by-units%* (special variable)
• *%use-single-replacement-paramodulation%* (special variable)
• *%use-sort-relativization%* (special variable)
• *%use-subsumption%* (special variable)
• *%use-subsumption-by-false%* (special variable)
• *%use-term-memory-deletion%* (special variable)
• *%use-term-ordering%* (special variable)
• *%use-term-ordering-cache%* (special variable)
• *%use-to-lisp-code%* (special variable)
• *%use-unit-restriction%* (special variable)
• *%use-ur-pttp%* (special variable)
• *%use-ur-resolution%* (special variable)
• *%use-variable-name-sorts%* (special variable)
• *%use-well-sorting%* (special variable)
• *%variable-sort-marker%* (special variable)
• *%variable-symbol-prefixes%* (special variable)
• *%variable-to-lisp-code%* (special variable)
• *%variable-weight%* (special variable)
• *snark-options* (special variable)
• finalize-options (function)
• initialize-options (function)
• options-have-been-critiqued (special variable)
• snark-option-spec-p (function)

3.1.18 snark-implementation/terms2.lisp

Dependency

options.lisp (file)

Parent

snark-implementation (system)

Location

src/terms2.lisp

Exported Definitions

• arg1 (compiler macro)
• arg1 (function)
• arg2 (compiler macro)
• arg2 (function)
• args (compiler macro)
• args (function)
• compound-p (compiler macro)
• compound-p (function)
• constant-p (compiler macro)
• constant-p (function)
• dereference (macro)
• head (compiler macro)
• head (function)
• make-compound (macro)
• make-compound* (macro)

Internal Definitions

• *=* (special variable)
• *a-function-with-left-to-right-ordering-status* (special variable)
• *a-function-with-multiset-ordering-status* (special variable)
• *and* (special variable)
• *answer-if* (special variable)
• *cons* (special variable)
• *exists* (special variable)
• *forall* (special variable)
• *frozen-variables* (special variable)
• *if* (special variable)
• *iff* (special variable)
• *implied-by* (special variable)
• *implies* (special variable)
• *not* (special variable)
• *or* (special variable)
• *xor* (special variable)
• arg1a (compiler macro)
• arg1a (function)
• arg2a (compiler macro)
• arg2a (function)
• argsa (compiler macro)
• argsa (function)
• compound-appl-p (compiler macro)
• compound-appl-p (function)
• dereference2 (macro)
• fancy-make-compound* (macro)
• head-or-term (compiler macro)
• head-or-term (function)
• heada (compiler macro)
• heada (function)
• make-a1-compound* (macro)
• make-compound%* (function)
• make-compound%2 (function)
• make-compound2 (function)
• make-tc (compiler macro)
• make-tc (function)
• prefer-to-bind-p (macro)
• tc-count (macro)
• tc-term (compiler macro)
• tc-term (function)
• unfrozen-variable-p (compiler macro)
• unfrozen-variable-p (function)
• variable-frozen-p (compiler macro)
• variable-frozen-p (function)

3.1.19 snark-implementation/rows.lisp

Dependency

terms2.lisp (file)

Parent

snark-implementation (system)

Location

src/rows.lisp

Exported Definitions

• last-row (function)
• map-rows (function)
• name-row (function)
• print-ancestry (function)
• print-rows (function)
• row (function)
• row (structure)
• row-ancestry (function)
• row-answer (function)
• (setf row-answer) (function)
• row-author (compiler macro)
• row-author (function)
• (setf row-author) (function)
• row-constraints (function)
• (setf row-constraints) (function)
• row-documentation (compiler macro)
• row-documentation (function)
• (setf row-documentation) (function)
• row-input-wff (compiler macro)
• row-input-wff (function)
• (setf row-input-wff) (function)
• row-level (function)
• row-name (compiler macro)
• row-name (function)
• (setf row-name) (function)
• row-name-or-number (function)
• row-number (function)
• (setf row-number) (function)
• row-parents (function)
• row-reason (function)
• (setf row-reason) (function)
• row-rewrites-used (function)
• (setf row-rewrites-used) (function)
• row-source (compiler macro)
• row-source (function)
• (setf row-source) (function)
• row-wff (function)
• (setf row-wff) (function)
• rows (function)

Internal Definitions

• *number-of-rows* (special variable)
• *row-count* (special variable)
• *row-names* (special variable)
• *rows* (special variable)
• *rowsets* (special variable)
• copy-row (function)
• initialize-rows (function)
• make-row (macro)
• make-row0 (function)
• make-rowset (function)
• map-rows-in-reason (function)
• mapnconc-rows (function)
• row-agenda-entries (function)
• (setf row-agenda-entries) (function)
• row-ancestry-rowset (function)
• row-bare-p (function)
• row-bare-unit-p (function)
• row-children (function)
• (setf row-children) (function)
• row-clause-p (function)
• row-conc-name (compiler macro)
• row-conc-name (function)
• (setf row-conc-name) (function)
• row-context (function)
• (setf row-context) (function)
• row-deleted-p (function)
• row-embedding-p (function)
• row-from-conjecture-p (function)
• row-given-p (function)
• row-hint-p (function)
• row-hints-subsumed (function)
• (setf row-hints-subsumed) (function)
• row-input-p (function)
• row-level0 (function)
• (setf row-level0) (function)
• row-negative-p (function)
• row-nonassertion-p (function)
• row-p (function)
• row-parent (function)
• row-plist (function)
• (setf row-plist) (function)
• row-positive-or-negative (function)
• (setf row-positive-or-negative) (function)
• row-positive-p (function)
• row-rewrites (function)
• (setf row-rewrites) (function)
• row-selections-alist (function)
• (setf row-selections-alist) (function)
• row-sequential (function)
• (setf row-sequential) (function)
• row-sequential-inheritably (function)
• row-status (function)
• (setf row-status) (function)
• row-subsumption-mark (function)
• (setf row-subsumption-mark) (function)
• row-supported (function)
• (setf row-supported) (function)
• row-supported-inheritably (function)
• row-unit-p (function)
• row-variables (function)
• row-wff-symbol-counts (function)
• row-wff-symbol-counts0 (function)
• (setf row-wff-symbol-counts0) (function)
• rows-in-reason (function)
• rowset-delete (function)
• rowset-empty? (function)
• rowset-insert (function)
• rowset-size (function)
• rowsets-delete (function)
• rowsets-delete-column (function)
• set-row-number (function)
• uninitialized (function)