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 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.