Default Reasoning

#$overrides is used when the assertions involved are general rules (axioms with quantifiers) and where those assertions will produce contradictory results in some situations. #$overrides makes it possible to resolve the contradictions by giving one of the assertions priority over the other.
To take a trite example:

P1 = "If something is a penguin, it can't fly."
P2 = "If something is a bird, it can fly."
P1 overrides P2.

#$exceptFor and #$exceptWhen are ``user interface'' predicates for stating rules about defaults. Statements using them are transformed into statements using #$abnormal by the system.
#$overrides   overrides

    The binary predicate #$overrides (which relates two instances of #$CycLAssertion) is used to tell Cyc which rule to prefer when it encounters two conflicting rules while reasoning with default assertions. (#$overrides FIRST SECOND) means that if the assertions FIRST and SECOND both appear in conflicting arguments for and against some proposition, the argument that contains FIRST is to be preferred.
    guid: bd58a273-9c29-11b1-9dad-c379636f7270
    direct instance of: #$AsymmetricBinaryPredicate #$TransitiveBinaryPredicate #$MetaKnowledgePredicate

#$exceptFor   except for    **COMMENT NOT REVIEWED**    **GAFs NOT REVIEWED**

    (#$exceptFor TERM ASSERTION) means that TERM is a thing, about which ASSERTION is known not to hold. #$exceptFor is a special case of #$exceptWhen (q.v.), applicable when ASSERTION has only one universally quantified variable. (#$exceptFor TERM ASSERTION) prevents TERM from binding to that variable, thereby blocking the conclusions about TERM that Cyc might otherwise draw from ASSERTION. In other words, if ASSERTION is an implication, then whatever proposition(s) -- call that Q -- that Cyc might have concluded about TERM from ASSERTION may or may not be true in Cyc, but (due to the exception) they would no longer be justified, even partially, by ASSERTION. Also, assertions made at the EL level with #$exceptFor are canonicalized into statements that do not reference #$exceptFor, but instead reference the predicate #$abnormal (see #$EmptinessOfAbnormalityNote). Note that the exception TERM should be a particular binding for the rule, not a collection, all of whose members the rule does not apply to.
    guid: bd65cd99-9c29-11b1-9dad-c379636f7270
    direct instance of: #$ExceptionRelation #$BinaryRelation

#$exceptWhen   except when

    This predicate relates a general assertion to a condition under which the assertion is known not to hold. More precisely, (#$exceptWhen FORMULA ASSERTION) means that FORMULA gives a condition under which ASSERTION fails to hold, and thus under which ASSERTION should not be used as justification for other inferences. In other words: ASSERTION holds, except (at least) in the case of FORMULA. Normally, ASSERTION is an (implicitly) universally quantified sentence, and FORMULA, in effect, places a restriction on the possible values of the universally quantified variables in ASSERTION. Since implicit universal quantification is interpreted as always having the widest possible scope, in the sentence (#$exceptWhen FORMULA ASSERTION) the free variables in ASSERTION are interpreted as if bound by quantifiers whose scope included the entire #$exceptWhen sentence. So any such variable in ASSERTION may also appear in FORMULA, and any of its occurrences in the latter are interpreted as if bound by the same wide-scope quantifier that binds the occurrences in ASSERTION. For example, if ASSERTION were (#$implies (#$isa ?THING #$GeographicalThing) (#$thereExists ?OTHER (#$northOf ?OTHER ?THING))) and FORMULA were (#$spatiallySubsumes #$NorthPole ?THING), the occurrence of the variable ?THING in the latter would be interpreted as if it were bound by the same wide-scope universal quantifer that binds the two occurrences of ?THING in the former. So the entire #$exceptWhen sentence would mean that every geographical thing has something to the north of it, except when the thing is spatially subsumed by the North Pole. A common special case of #$exceptWhen is handled by #$exceptFor (q.v.). Note that assertions made at the EL level with #$exceptWhen are canonicalized into statements that do not contain #$exceptWhen, but instead contain the predicate #$abnormal (see #$EmptinessOfAbnormalityNote.)
    guid: bd595e7e-9c29-11b1-9dad-c379636f7270
    direct instance of: #$ExceptionRelation #$BinaryRelation

#$abnormal   abnormal (default monotonic predicate) (binary predicate) (CycL predicate)    **COMMENT NOT REVIEWED**    **GAFs NOT REVIEWED**

    Every default rule in our system P(x1,...,xn) => Q(x1,...,xn) is implicitly treated as (not(abnormal(x1,...,xn)) and P(x1,...,xn) => Q(x1,...,xn) This allows rules without exceptions to never have to incur the overhead of default reasoning. Exceptions to rules are written like so: (#$exceptWhen R(x1,...,xn) Rule001) and get canonicalized into rules concluding abnormal like so: R(x1,...,xn) => (#$abnormal(x1,....,xn) Rule001) Since a different 'abnormality' predicate is needed for every default rule in the system, we instead handle this uniqueness requirement by having a single #$abnormal predicate which takes the rule in question as an argument. Also, the variables over which abnormality is computed is given as a single list. This allows #$abnormal to be binary rather than arbitrary arity.
    guid: bd5880bd-9c29-11b1-9dad-c379636f7270
    direct instance of: #$BinaryPredicate #$DefaultMonotonicPredicate

#$NoteAboutStatingExceptionsInCycL   note about stating exceptions in cyc l    **COMMENT NOT REVIEWED**    **GAFs NOT REVIEWED**

    The formula (#$exceptWhen P(?x0 ... ?xn) Q(?x0 ... ?xn))) states that, in situations where assertion Q would apply to a set of bindings for variables ?x0 ... ?xn, the conclusion is allowed `except when' P(?x0 ... ?xn) is true for these variable bindings. The formula (#$exceptFor [term] Q(?x0)) states that, in situations where assertion Q would apply to a variable ?x0, the conclusion is allowed `except for' the situations where [term] is the binding for ?x0. To be well-formed, Q must be a rule with exactly one free variable. By definition, #$exceptFor is merely syntactic sugar: (#$exceptFor [term] Q(?x0)) <=> (#$exceptWhen (equals ?x0 [term]) Q(?x0)) Since an #$exceptWhen statement is a meta-statement about some rule Q(?x0 ... ?xn), the statement is not well-formed if Q(?x0 ... ?xn) is not already an assertion in the KB. Also, strictly speaking, P and Q in the #$exceptWhen merely must share some variables rather than all variables as it's been written above. These constructs replace `abnormal' at the EL (epistemological level). Old assertions of the form: (#$implies P(?x0 ... ?xn) (abnormal R(?x0 ... ?xn) Q(?x0 ... ?xn))) become: (#$exceptWhen P(?x0 ... ?xn) Q(?x0 ... ?xn)) The predicate `abnormal' has not actually gone away, but was modified for use as the HL (Heuristic Level) implementation of #$exceptWhen. Like #$termOfUnit, `abnormal' should be viewed as an inference-maintained predicate, and human beings should not be manually asserting things using `abnormal.' ;;; ;; EXAMPLES ;;; Rule1: `birds fly' (#$implies (#$isa ?BIRD #$Bird) (#$behaviorCapable ?BIRD #$Flying-FlappingWings #$performedBy) Exception1: `for penguins, the ``birds fly'' rule does not apply' (#$exceptWhen (#$isa ?BIRD #$Penguin) [Rule1]) Exception2: `the ``birds fly'' rule does not apply to Tweety' (#$exceptFor Tweety [Rule1]) Exception3: `for an animal with an injured wing, the ``birds fly'' rule does not apply' (#$exceptWhen (#and (#$anatomicalParts ?BIRD ?WING) (#$isa ?WING #$Wing-AnimalBodyPart) (#$hasPhysiologicalAttributes ?WING #$Injured) [Rule1]) Rule2: ``dogs who like the same cat like each other'' (#$implies (?and (#$isa ?DOG1 #$Dog) (#$isa ?DOG2 #$Dog) (#$isa ?CAT #$Cat) (#$likesAsFriend ?DOG1 ?CAT) (#$likesAsFriend ?DOG2 ?CAT)) (#$likesAsFriend ?DOG1 ?DOG2)) Exception3: `Rex does not like other dogs according to ``Rule2''' (#$exceptWhen (#$equals ?DOG1 Rex) [Rule2]) Exception4: `Fifi is not liked by other dogs according to `Rule2''' (#$exceptWhen (#$equals ?DOG2 Fifi) [Rule2]) Exception5: `Morris is not such a cat according to ``Rule2''' (#$exceptWhen (#$equals ?CAT Morris) [Rule2])
    guid: be660580-9c29-11b1-9dad-c379636f7270
    direct instance of: #$SharedNote #$Individual

#$MetaAssertionsForPolyCanonicalizingAssertions   meta assertions for poly canonicalizing assertions    **COMMENT NOT REVIEWED**    **GAFs NOT REVIEWED**

    If one wishes to state a fact M about an formula F, i.e. if one wishes to assert the meta-assertion M(F) and if F canonicalizes into multiple assertions, a_1, a_2...a_n, then one may have to do a non-standard procedure. If F canonicalizes into a_1, a_2...a_n *and* when any of a_1, a_2...a_n uncanonicalize back into F then the meta assertion M(F) gets automatically distributed to each of a_1, a_2...a_n. In such a case M(F) ends up in the knowledge base as several assertions, i.e. M(a_1), M(a_2), ... M(a_n). In other cases (i.e. where a polycanonicalizing formula does not uncanonicalize back into itself) (typically rarer), one will have to do the non-standard procedure of distributing the meta-assertions by hand. Example (of the more standard case): (fi-assert '(#$implies (#$isa ?x #$Animal) (#$thereExists ?y (#$and (#$isa ?y #$FemaleAnimal) (#$mother ?x ?y)))) #$BaseKB) produces in the two assertions: #(#$and (#$isa ?X #$Animal) (#$termOfUnit ?Y (SKF-16480338 ?X))) (#$mother ?X ?Y)):#$BaseKB> #(#$and (#$isa ?X #$Animal) (#$termOfUnit ?Y (SKF-16480338 ?X))) (#$isa ?Y #$FemaleAnimal)):#$BaseKB> Note that these two assertions share the common EL formula: (#$implies (#$isa ?x #$Animal) (#$thereExists ?y (#$and (#$isa ?y #$FemaleAnimal) (#$mother ?x ?y)))) Now if we add a meta assertion that references this formula: (fi-assert '(#$salientAssertions #$mother (#$implies (#$isa ?x #$Animal) (#$thereExists ?y (#$and (#$isa ?y #$FemaleAnimal) (#$mother ?x ?y))))) #$BaseKB) the meta formula automatically distributes over the two assertions: #(#$and (#$isa ?X #$Animal) (#$termOfUnit ?Y (SKF-16480338 ?X))) (#$mother ?X ?Y)):#$BaseKB):#$BaseKB> #(#$and (#$isa ?X #$Animal) (#$termOfUnit ?Y (SKF-16480338 ?X))) (#$isa ?Y #$FemaleAnimal)):#$BaseKB):#$BaseKB> This new behavior was added to the system on December 9, 1998. It can be turned-off by setting the parameter CYC::*DISTRIBUTE-META-OVER-COMMON-EL?* to nil.
    guid: bfb7415a-9c29-11b1-9dad-c379636f7270
    direct instance of: #$SharedNote #$Individual