: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))).
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].)
Suppresses rule completion (see section 2.3.1).