next up previous contents index
Next: Control Structure Up: Special Forms Previous: Controlled Retrieval

Negation and Non-Monotonic Reasoning

Non-monotonic reasoning is still a research topic in Algernon. To use non-monotonic forms like :unp and :assume successfully, you will probably have to understand something of the internals of how Algernon does inference (see section 2.3).

(:neq  fterm1 fterm2)

Succeeds iff fterm1 tex2html_wrap_inline1522 fterm2. (:neq fterm1 fterm2) is equivalent to (:eval (not (eql 'fterm1 'fterm2))).

(:fail  . path)
(:unp  . path)

Unprovable. Succeeds exactly when a query of path fails. :unp is used primarily in default rules. For example:

(:rules Birds
 ((flies ?x True) <- (:unp (not (flies ?x True)))
                     (:assume (normal ?x Birds flies))))
(:assume is discussed below).

The idiom (:fail (:retrieve atomic-formula)) succeeds if atomic-formula is not explicitly stored in the knowledge base, without applying any rules.

(:assume  atomic-formula)

Adds atomic-formula to the knowledge-base as an assumption. Assumptions differ from facts in two ways. First, an attempt is made to prove the negation of the atomic-formula, and if this attempt succeeds, the :assume fails. Second, any future conclusion which depends on the assumption is tagged with the assumption, so that if the assumption is later withdrawn the conclusion is also withdrawn.

Micheal S. Hewett
Tue Oct 29 11:28:38 CST 1996