In any sufficiently rich human-crafted knowledge base, there will be many propositions P for which
you cannot prove PIn general, the failure to prove P is not a sound basis for concluding (not P), i.e., that P is false. Nevertheless, it is sometimes useful to permit this conclusion to be tentatively drawn. Negation-by-failure is the inference rule that allows this. (Note that 'not' in CycL is the operator for classical negation; it is not a symbol for negation-by-failure.)
you cannot prove (not P).
In CycL there are currently only two instances where negation-by-failure is always used, and each is a specific well-defined instance of the Closed World Assumption:
(1) if P is a literal of the form
(equals <constant1> <constant2>)then the lack of a proof of P is sufficient to prove (not P). This is the CycL implementation of the Unique Names Assumption.
(2) if P is a literal of the form
(abnormal <bindings> <rule>)then the lack of a proof of P is sufficient to prove (not P). This is the CycL implementation of the policy of minimizing abnormalities.
CycL does provide other mechanisms for using negation-by-failure to establish negations which are under the user's control.
The first mechanism is the use of meta-statements about known limits of our knowledge to conclude that certain assertions are not true. For example, if we list the 12 men who have walked on the moon, it's useful to be able to state that we know that our knowledge on this subject is complete. We can then conclude in one fell swoop via this meta-knowledge that all the other billions of humans have not walked on the moon.
Thus, in situations where we know that a particular collection has its full extent realized, or a particular relation has its full extent realized, we can use the lack of an argument for an assertion being true as a relatively strong argument for it not being true.
The two supported predicates used for stating complete extent knowledge are:
#$completeCollectionExtent #$completeExtentKnownHL modules supporting these two predicates are always enabled. As a result, they are typically used in relatively specific microtheories which are known to contain certain complete representations of knowledge.
For example by asserting :
In UnitedStatesGeographyMt : (#$completeCollectionExtent #$State-UnitedStates) In RandMcNallyAtlasMt : (#$completeExtentKnown #$bordersOn)we now have relatively strong arguments for negations such as :
(#$not (#$isa #$Manitoba #$State-UnitedStates)) in the UnitedStatesGeographyMtand
(#$not (#$bordersOn #$France #$Taiwan)) in the RandMcNallyAtlasMt.
You can contrast the usage of #$completeExtentKnown with that of #$unknownSentence, which itself does not indicate negation. Circumscription (through the use of #$completeExtentKnown) effectively turns an #$unknownSentence into a #$not.
The second mechanism allows the user to enable the broader use of negation-by-failure as an inference method. The inference parameter
*NEGATION-BY-FAILURE*defaults to NIL and controls whether or not negation-by-failure is used more broadly. When this parameter is enabled, support for #$minimizeExtent is turned on. For example, asserting
(#$minimizeExtent #$geographicalSubRegions)would indicate that we will use the failure to prove P as a weak argument for P whenever the predicate is #$geographicalSubRegions. In addition, when this parameter enabled, all collections are minimized, providing weak arguments for
(#$not (#$isa #$Foo #$Bar))whenever
(#$isa #$Foo #$Bar)is not already known to be true.
Whenever (not P) is concluded by negation-by-failure, this fact is explicitly noted. During argumentation negation-by-failure is taken to be an extremely weak argument for (not P) -- so weak, in fact, that any other argument should outweigh it when they are adjudicated. Thus, there is an important difference between the assertion (not P) and the conclusion that (not P) is true by negation-by-failure. The latter behaves as an assumption.
If assuming not(P) leads to a contradiction, then the set of assertions involved in the contradiction form a reductio ad absurdum proof of P. In fact, if P can ever be established, then the assumption that (not P) must be retracted, and via truth maintenance all conclusions derived from it must also be retracted.
Using a general minimization inference method tied with assumptions and argumentation, Cyc's behavior when asked whether something is not true will mirror the kind of belief revision behavior that a human typically exhibits. Consider the following example:
(Fact1) My god-daughter's mother used to pat some bald guy named Ed on the head during church when she was little.
(Q) Did Ed ever walk on the moon?
There are two rational answers:
(A) Huh? I have no idea. (the fact has nothing to do with the question)
(A) No, probably not. (a safe assumption: almost nobody has, anyway)
Which answer is better depends on the situation (i.e. is application-specific). It's nice to have user control over which to say, just like a person does.
(Fact2) That occurred in 1968, and Ed was none other than Edwin "Buzz" Aldrin, the lunar module pilot of Apollo 11.
(Q) Did Ed ever walk on the moon?
(A) Yes! (I didn't realize until now that you were referring to THAT Ed).
All we had to do to gracefully handle the above apparent contradiction was to use assumptions and belief revision in a straightforward, natural manner. CycL will do the same.
Finally, each such inference implementation "decision" like
"Are we using the Unique Names Assumption?"is independently under the user's control via inference parameters which the user can choose to turn on or off.
"Are we minimizing abnormalities?"
"Are we allowing assumption-based negation minimization?"
"Do we allow positive assumptions?"
...