Controlling Style of Inference

(:retrieve  atomic-formula)

(:db  atomic-formula)

:retrieve (and its synonym :db) succeeds if the atomic-formula is already in the knowledge base. It does not apply any further rules to attempt to deduce the atomic-formula. :retrieve should be used only in queries. It distributes over functional forms: ((:retrieve (p (f ?x) ?y))) expands to ((:retrieve (f ?x ?$X2)) (:retrieve (p ?$X2 ?y))).

(:w-contra-positive  . path)

(:wo-contra-positive  . path)

These forms are used to enable and disable the addition to the knowledge-base of the contra-positives of rules. The default is not to add contra-positives. Contra-positives are used to minimize proofs by contradiction when reasoning with disjunctions. (An example of the use of disjunction is given in [Crawford, 90].)

(:no-completion  . path)

Suppresses rule completion (see section 2.3.1).