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`is equivalent to*fterm1 fterm2*)`(: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`succeeds if*atomic-formula*))*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.

Tue Oct 29 11:28:38 CST 1996