Implicit Cyc Functionality

11.1. TMS: Truth Maintenance System

11.1.1. What is TMS?

Any time Cyc learns a piece of new information, it could potentially contradict any other fact that Cyc already knows. Conversely, any time Cyc learns that a piece of information it once held to be true is in fact not the case, this could potentially undermine any of Cyc's knowledge. It is infeasible for Cyc to reconsider every assertion in its knowledge base every time it learns or unlearns a new piece of information; also it is infeasible for all of the dependencies between assertions to be declaratively stored. The compromise is Cyc's Truth Maintenance System (TMS).

11.1.2. How TMS is stored internally

The KB datastructures relevant to TMS are arguments, deductions, beliefs, supports, and assertions. Here are a couple of graphs explaining their relationships to each other. The diagonal lines are genls links and the dashed arrow is a "contains many" link.

            argument         
           /        \      
     belief         deduction  - - - - - ->  support
      /                                     /       \
asserted argument                   assertion       hl-support

Every assertion in the KB is justified by at least one argument. A belief is an unjustified argument. Currently the most common belief is an asserted argument, which says, effectively, "because somebody told me so." A deduction is basically a set of supports which constitute a deductive proof for the assertion they justify.

For example, if we had an argument justifying the assertion

  (isa Lassie Dog)

in the BiologyMt,

a reasonable set of supports for this argument might be the assertion

  (isa Lassie Collie)

in the BiologyMt,

and the rule

  (implies
    (isa ?X Collie)
    (isa ?X Dog))  

in the BaseKB.

However, reasoning of this sort is actually done via SBHL, not by explicit rules. So a more realistic support for this argument would be

  :ISA (isa Lassie Collie) 

in BiologyMt

which is an HL support, telling us that the :ISA HL TMS module supports the assertion. HL supports will be discussed in more detail later.

11.1.3. Argumentation

Argumentation is how Cyc deals with possibly contradictory information when it is added to its knowledge base. It looks at the set of arguments which are supporting an assertion or its negation, and attempts to adjudicate which should win out. Here is the algorithm it uses to adjudicate.

If there's only one argument, it wins.
Otherwise, we know we have more than one argument.
If all the arguments have the same truth and strength (strength being either default or monotonic), then the assertion's truth and strength are determined by that of the arguments.
Otherwise, we know we have differing arguments.
If Cyc has both a monotonically true and a monotonically false argument for an assertion, this currently produces an error.
Otherwise, we know that we don't have a hard contradiction.
If there is a monotonic argument for an assertion, the monotonic argument wins.
Otherwise, we know that we don't have any monotonic arguments, only default arguments.
If there is a belief argument (and there can be at most one), it takes precedence over a deduced argument.
Otherwise, we know that we have only default deduced arguments -- no monotonic arguments and no belief arguments.
If we have a true argument but lack a false argument, deem the assertion true.
If we have a false argument but lack a true argument, deem the assertion false.
Otherwise, one of two cases obtains: (1) we have at least one default deduced true argument and one default deduced false argument, or (2) all arguments have a truth value of "unknown".
At this point, Cyc gives up and deems the assertion unknown.

11.1.4. Immediate TMS (the "ripple effect")

We assume that the KB begins in a consistent TMS state. When an argument is added or removed from an assertion, it is a belief revision step for the KB. First the arguments for that assertion are reconsidered, and the assertion may or may not change truth value or strength. If it changes, then Cyc looks at all the assertions supported by the newly changed assertion, and continues to ripple outward until quiescence. It's guaranteed to terminate, because TMS does not add new deductions or assertions, it only changes them or removes them, and the changing is done in such a way that infinite oscillation is impossible.

When an argument is added or removed from an assertion, argumentation is triggered on that assertion, as explained above. If argumentation changes the truth value of the assertion, then all the arguments which were previously justified by this assertion are invalidated (removed), which may trigger more argumentation and TMS. If argumentation changes the strength of the assertion but leaves its truth value intact, then TMS is triggered to reexamine the strengths of the deductions in which it is a support.

If the last argument is removed from an assertion, this means that the assertion now has a truth value of "unknown". At this point there is no longer any advantage to explicitly representing the assertion in the KB, so it is removed.

11.1.5. Deep TMS

Argumentation is triggered each time an argument is added or removed from an assertion, and if if this changes the truth value or strength of the assertion, Immediate TMS (discussed above) is triggered. However, the "ripple effect" of Immediate TMS only ripples outward through assertions and deductions; it does not reexamine HL supports. Hence, HL supports can be made false without triggering Immediate TMS. This, in addition to its rippling nature (the fact that it acts locally, not globally) is why Immediate TMS is incomplete. To find and re-examine assertions with HL supports that are no longer valid, Immediate TMS is not enough; we need Deep TMS.

For example, if we had the following HL support in a deduction supporting some assertion,

  :GENLS (genls Collie Animal)

in BiologyMt

there are a vast number of #$genls assertions which, if removed, could make this HL support false. For example:

  (genls Collie Dog)
  (genls Dog CanineAnimal)
  (genls CanineAnimal NonPersonAnimal)
  (genls NonPersonAnimal Animal)

If any of the above assertions were removed, the aforementioned HL support would no longer be valid. However, this TMS information is not stored, because representing it all explicitly would take an explosive amount of storage space. Furthermore, if any of these #$genls assertions were removed in the chain between #$Poodle and #$Animal, Immediate TMS would not be triggered; Deep TMS is needed to detect the staleness. This is one of the tradeoffs of Cyc's TMS implementation. You can trigger Deep TMS by the [Force TMS] or [Redo TMS] buttons in the Cyc Browser.

Here's a more concrete example of how TMS could go stale and the [Force TMS] button would have an effect.

In the NaivePhysicsMt, create two collections RedThing and CrimsonThing, and make CrimsonThing a spec of RedThing. Assert the forward rule

  (implies
    (isa ?OBJ RedThing)
    (objectHasColor ?OBJ RedColor))

Then create a new constant CrimsonThing212, and make it an instance of CrimsonThing. The forward rule will be triggered, and this assertion

  (objectHasColor CrimsonThing212 RedColor)

will be deduced. Its supports will be:

  1.  (implies
           (isa ?OBJ RedThing)
           (objectHasColor ?OBJ RedColor)) in NaivePhysicsMt
  2.  (isa CrimsonThing212 CrimsonThing) in NaivePhysicsMt
  3.  :GENLS (genls CrimsonThing RedThing) in NaivePhysicsMt

Now if we unassert

  (genls CrimsonThing RedThing)

the deduced assertion

  (objectHasColor CrimsonThing212 RedColor)

remains in the KB, because TMS revalidation of HL supports is not automatically triggered. If you [Redo TMS] on the assertion, or [Force TMS] on CrimsonThing212, the stale assertion will be reexamined by TMS, the SBHL will find that the genls link no longer holds, and since that was the only argument for that assertion, the assertion's truth value will become "unknown", and it will be removed.

11.2. SubL Interactor

SubL is the underlying implementation language of Cyc. The SubL Interactor is an interface into the guts of the Cyc system. It is a read-eval-print window, which means that it will read in whatever SubL expression you type in, evaluate it (which may perform some side effects), and print out the results of the evaluation.

The SubL interactor prints the same results as one would get upon evaluating a SubL function at the read loop in the Cyc buffer, with one exception, namely, in the SubL interactor, HTML tags are interpreted by the browser in accord with the constant browser ("cb") interface functions, but are simply printed at the read loop.

For example, at the read loop, (find-assertion-by-id 772452) returns:

   #<AS:(#$superTaxons #$Dog #$CanineAnimal):#$BiologyVocabularyMt>

In the SubL interactor, (find-assertion-by-id 825989) returns:

  (superTaxons Dog Canine Animal)

The intent of the SubL Interactor is to allow OEers who have an understanding of Cyc's code base to execute scripts or commands via the Cyc Browser.

A good source for useful SubL functions can be found at: http://www.cyc.com/cyc-api.html

No more documentation on it is provided because familiarity with the Cyc code base is assumed.

Example:

Type in

  (constant-name #$Dog)

click on Eval

yields

  "Dog"

11.3. Current HL Modules

Currently (August 2001) there are 495 HL modules in the Cyc Inference Engine. This section will describe some of the most commonly used HL modules, and give a listing of the rest. A more complete, up-to-date, and hypertext-indexed description of each HL module is available in the Cyc Browser, from the Nav page, via the link "HL Module Summary". This document provides a better overview, and the browser provides better details. A few examples of the cases covered by the classes of HL modules are given here; a more complete listing of cases and examples can be found on the HL Module Summary page.

The most important distinction is between removal modules, transformation modules, and forward modules. These three types of HL modules partition the HL module space. Furthermore, an important partition of the removal module space is between removal modules which are predicate-specific and those which are generic. Evaluatable predicates and functions are like predicate-specific removal modules with a very stylized form.

The genls graph under #$CycHLModule in the KB yields a much prettier version of the following hierarchy:

                     ________HL module________
                    /            |            \
Transformation module      Removal module     Forward module
                          /              \
       Generic Removal module        Predicate-specific removal module

First, we will cover the generic removal modules, which could apply to any predicate in the KB.

11.3.1. Generic Removal Modules

11.3.1.a. Basic Lookup

These are the removal modules that support the basic low-level lookup methods.

Examples:

  • (#$bordersOn #$UnitedStatesOfAmerica ?COUNTRY)
  • (#$bordersOn #$UnitedStatesOfAmerica #$Canada)
  • (?PREDICATE #$UnitedStatesOfAmerica #$Canada)

11.3.1.b. SBHL modules

These are the SBHL modules, which support reasoning using #$genlPreds, #$genlInverse, and #$negationPreds.

Examples:

  • (#$spatiallyIntersects #$ContinentOfEurope #$CityOfParisFrance)
  • (#$not (#$spatiallyIntersects ?WHAT ?WHAT-ELSE))
  • (#$spatiallyIntersects ?WHAT ?WHAT-ELSE)

11.3.1.c. Reflexivity and Irreflexivity

(#$notFarFrom #$Italy #$Italy)

in

#$WorldGeographyMt

via

(#$isa #$notFarFrom #$ReflexiveBinaryPredicate)

 

(#$not (#$farFrom #$Italy #$Italy))

in

#$WorldGeographyMt

via

(#$isa #$farFrom #$IrreflexiveBinaryPredicate)

11.3.1.d. Symmetry and Asymmetry

(#$not (#$northOf #$UnitedStatesOfAmerica #$Canada))"
(#$bordersOn #$Canada #$UnitedStatesOfAmerica)"

11.3.1.e. Transitivity

(#$geographicalSubRegions ?SUPER #$CityOfParisFrance)
(#$geographicalSubRegions #$ContinentOfEurope ?SUB)
(#$geographicalSubRegions #$ContinentOfEurope #$CityOfParisFrance)

11.3.1.f. #$transitiveViaArg(Inverse)

The system will attempt to use #$transitiveViaArg(Inverse) assertions to prove or provide bindings for your query. This applies any time the predicate in question has any #$transitiveViaArg(Inverse) assertions on it, or if some spec-pred of the predicate has some #$transitiveViaArg(Inverse) assertions on it.

Example:

 (#$relationAllExists #$physicalParts #$Dog #$Head)

via

 (#$relationAllExists #$anatomicalParts #$Vertebrate #$Head-Vertebrate)

and

 (#$transitiveViaArg #$relationAllExists #$genlPreds 1)
 (#$transitiveViaArgInverse #$relationAllExists #$genls 2)
 (#$transitiveViaArg #$relationAllExists #$genls 3)
 (#$genlPreds #$anatomicalParts #$physicalParts)
 (#$genls #$Dog #$Vertebrate)
 (#$genls #$Head-Vertebrate #$Head)

11.3.1.g. #$relationAllExists, #$relationExistsAll

Examples:

  • (#$citizens ?WHERE #$AbrahamLincoln)

    from

    (#$relationExistsAll #$citizens #$Country #$Person)

    and

    (#$isa #$AbrahamLincoln #$Person)
  • (#$grandfathers #$AbrahamLincoln ?RELATIVE)

    from

    (#$relationAllExists #$grandfathers #$Animal #$MaleAnimal)
    

    and

    (#$isa #$AbrahamLincoln #$Animal)

11.3.1.h. #$relationAll, #$relationAllInstance, #$relationInstanceAll

Examples:

  • (#$hasGender #$AbrahamLincoln #$Masculine)

    from

    (#$relationInstanceAll #$hasGender #$MalePerson #$Masculine)

    and

    (#$isa #$AbrahamLincoln #$MalePerson)
  • (#$temporallyContinuous #$AbrahamLincoln)

    from

    (#$relationAll #$temporallyContinuous #$Entity)

    and

    (#$isa #$AbrahamLincoln #$Entity)

11.3.1.i. #$completeExtentKnown, #$minimizeExtent

  • (#$not (#$bordersOn #$Canada #$France))

    from

     (#$completeExtentKnown #$bordersOn)
  • (#$not (#$citizens #$AbrahamLincoln #$France))

    from

     (#$minimizeExtent #$citizens)

See the section on Negation By Failure Reasoning for more information on these.

11.3.1.j. Evaluatable predicates

There is one generic removal module for all evaluatable predicates (see #$evaluationDefn). The evaluatable predicates themselves are covered in their own section, below.

11.3.2. Predicate-specific removal modules:

The following predicates have one or more removal modules defined to handle inference with that specific predicate.

11.3.2.a. SBHL Predicates

    • #$isa
    • #$genls
    • #$genlPreds
    • #$genlInverse
    • #$genlMt
    • #$genlAttributes
    • #$disjointWith
    • #$negationPreds
    • #$negationInverse
    • #$negationAttribute
    • #$nearestIsa
    • #$nearestGenls
    • #$nearestGenlPreds
    • #$nearestGenlMt
    • #$nearestGenlAttributes
    • #$nearestCommonIsa
    • #$nearestCommonGenls
    • #$nearestCommonSpecs
    • #$nearestCommonGenlMt
    • #$nearestDifferentIsa
    • #$nearestDifferentGenls

11.3.2.b. SBHL-Time Predicates

    • #$contiguousAfter
    • #$cotemporal
    • #$endsAfterEndingOf
    • #$endsAfterStartingOf
    • #$endsDuring
    • #$endingDate
    • #$overlapsStart
    • #$startingDate
    • #$startsAfterEndingOf
    • #$startsAfterStartingOf
    • #$startsDuring
    • #$temporalBoundsContain
    • #$temporalBoundsIdentical
    • #$temporalBoundsIntersect
    • #$temporallyCooriginating
    • #$temporallyCoterminal
    • #$temporallyDisjoint
    • #$temporallyFinishedBy
    • #$temporallyIntersects
    • #$temporallyStartedBy
    • #$temporallySubsumes
    • #$birthDate
    • #$dateOfDeath
    • #$dateOfEvent

11.3.2.c. Other HL-supported predicates

  • Equality-related predicates
    • #$different
    • #$differentSymbols
    • #$equalStrings-CaseInsensitive
    • #$equalSymbols
    • #$equals
    • #$indexicalReferent
  • Set-related predicates
    • #$elementOf
    • #$nthLargestElement
    • #$nthSmallestElement
    • #$subsetOf
    • #$extentCardinality
  • Context lifting predicates
    • #$ist
  • Important Cyc-internal predicates
    • #$evaluate
    • #$termChosen
    • #$performSubL
  • Well-formedness predicates
    • #$admittedArgument
    • #$admittedSentence
  • Inheritance-blocking predicates
    • #$assertedPredicateArg
    • #$assertedSentence
    • #$ist-Asserted
    • #$assertedTermSentences
  • Predicates relating CycL terms to their properties
    • #$constantName
    • #$constantID
    • #$assertionID
    • #$assertionJustificationAttribute
    • #$assertionMt
    • #$assertionSentence
    • #$natFunction
    • #$natArgument
    • #$natArgumentsEqual
    • #$termOfUnit
    • #$termFormulas
  • Truth-related predicates
    • #$knownSentence
    • #$unknownSentence

    • #$trueSentence
    • #$sentenceEquiv

    • #$sentenceImplies
    • #$consistent
  • NL-related predicates
    • #$termPhrases
    • #$termStrings
    • #$wordForms
    • #$wordStrings
  • Application-motivated predicates
    • #$programFoundOnComputer
    • [and others for CycSecure]
  • Miscellaneous predicates
    • #$conceptuallyRelated
    • #$integerBetween

11.3.3. Evaluatable Predicates

Here is the list of evaluatable predicates currently in the system. See the HL Module Summary page for more information.

  • Equality-related predicates
    • #$different
    • #$differentSymbols
  • Date-related predicates
    • #$dateSubsumes
    • #$laterThan
  • Quantity-related predicates
    • #$greaterThan
    • #$greaterThanOrEqualTo
    • #$lessThan
    • #$lessThanOrEqualTo
    • #$numericallyEqual
    • #$quantityIntersects
    • #$quantitySubsumes
  • List predicates
    • #$initialSublists
    • #$listSetMembers
    • #$sublists
  • String predicates
    • #$stringSubword
    • #$substring
    • #$substring-CaseInsensitive
  • SubL predicates
    • #$trueSubL
  • Application-specific predicates
    • #$programInVersionSeries
    • #$versionOfProgram
    • [and more for CycSecure]

11.3.4. Evaluatable Functions

  • Arithmetic functions
    • #$PlusFn
    • #$DifferenceFn
    • #$MinusFn
    • #$AbsoluteValueFn
    • #$TimesFn
    • #$QuotientFn
    • #$Percent
    • #$InverseOfIntervalFn
    • #$SquaredFn
    • #$SqrtFn
    • #$LogFn
    • #$ExpFn
    • #$ExponentFn
  • Rounding functions
    • #$RoundDownFn
    • #$RoundUpFn
    • #$RoundClosestFn
  • Summation and related functions
    • #$PlusAll
    • #$TimesAll
    • #$Minimum

    • #$Maximum
    • #$Average
  • Trigonometric functions
    • #$SineFn
    • #$CosineFn
    • #$TangentFn
    • #$CosecantFn
    • #$SecantFn
    • #$CotangentFn
    • #$ArcSineFn
    • #$ArcCosineFn
    • #$ArcTangentFn
    • #$ArcCosecantFn
    • #$ArcSecantFn
    • #$ArcCotangentFn
  • Date functions
    • #$DateBeforeFn
    • #$DateAfterFn
    • #$DateFromIntegerFn
  • CycL manipulation functions
    • #$FormulaArityFn
    • #$FormulaArgFn
    • #$FormulaArgSetFn
    • #$FormulaArgListFn
    • #$SubstituteFormulaFn
    • #$SubstituteFormulaArgFn
    • #$AssertionAssertTimeFn
    • #$RelationTuplesFn
  • Set and List functions
    • #$SetIntersection
    • #$SetExtentFn
    • #$SetOfListMembersFn
    • #$JoinSimpleListsFn
    • #$LengthOfListFn
    • #$NthInListFn
    • #$JoinListsFn
    • #$FirstInListFn
    • #$RestOfListFn
    • #$LastInListFn
    • #$SublistFromToFn
    • #$PositionsInListFn
    • #$ReverseListFn
  • String functions
    • #$LengthOfStringFn
    • #$SubstringFn
    • #$StringToIntegerFn
    • #$IntegerToStringFn
    • #$StringConcatFn
    • #$StringTokenizeFn
    • #$StringPostremoveFn
    • #$StringPreremoveFn
    • #$StringReplaceSubstringFn
  • ScalarInterval functions
    • #$QuantityConversionFn
    • #$MinRangeFn
    • #$MaxRangeFn
    • #$ToleranceFn
    • #$MinQuantValueFn
    • #$MaxQuantValueFn
  • NL functions
    • #$UniqueWordSenseFn
    • #$StringsToPhraseFn
    • #$SubstituteNLTEFn
    • #$DavidsonianFn
    • #$EnglishSuffixFn
  • Miscellaneous functions
    • #$IdentityFn
    • #$EvaluateSubLFn

11.3.5. Transformation Modules

There are currently (August 2001) 10 transformation modules in the Cyc Inference Engine. These are used to transform a literal P into another set of literals (possibly a singleton, possibly more), such that if we can prove this set of literals, we can therefore prove P.

11.3.5.a. Backchaining

The most commonly used transformation module is backchaining, which uses, to state a simple case, the literal P and the rule Q -> P to transform P to Q. Recall that instead of a single literal Q, P may be transformed into a set of literals.

Example:

(#$likesAsFriend #$AbrahamLincoln ?WHO)

from a rule concluding to #$likesAsFriend

Another case of backchaining is backchaining on an unbound predicate. For pedagogical purposes, say we implemented the HL support for #$SymmetricBinaryPredicate via a rule instead of an HL module. The rule would be this:

  (#$implies
    (#$and
      (#$isa ?PRED #$SymmetricBinaryPredicate)
      (?PRED ?ARG1 ?ARG2))
    (?PRED ?ARG2 ?ARG1))

which has a consequent with a variable in the arg0 position. Hence, this rule can be backchained on any time the literal matches the consequent. In this case, all that is necessary is for the literal to be binary. For example, if we were trying to prove

  (#$bordersOn #$Canada #$France)

we might have to backchain on the above rule, and instead try to prove

  (#$and
    (#$isa #$bordersOn #$SymmetricBinaryPredicate)
    (#$bordersOn #$France #$Canada))

Unbound predicate backchaining can be computationally explosive because it has enormous syntactic applicability, and the syntactic information is all the transformation module uses to determine when to backchain. Due to this explosiveness, its use is gated by an inference parameter which is default off.

11.3.5.b. Symmetry and Asymmetry

(#$bordersOn #$Canada ?WHAT)

from

(#$isa #$bordersOn #$SymmetricBinaryPredicate)

and a rule concluding to #$bordersOn

(#$not (#$northOf ?WHAT #$Canada))

from

(#$isa #$northOf #$AsymmetricBinaryPredicate)

and a rule concluding to #$northOf

11.3.5.c. SBHL overrides

By tweaking the advanced inference settings, you can choose to enable these transformation modules instead of using the SBHL predicates, so that, for instance, you can prove #$isa statements via rules.

(#$isa #$AbrahamLincoln #$FamousPerson)

from

(#$genls #$UnitedStatesPresident #$FamousPerson)

and a rule concluding to #$isa #$UnitedStatesPresident

(#$not (#$isa #$AbrahamLincoln #$FrenchPerson))

from

(#$genls #$FrenchPerson #$EuropeanPerson)

and a rule concluding from #$isa #$EuropeanPerson

11.3.5.d. Exception handling

There is a special transformation module for #$abnormal, to handle exceptions in inference.

11.3.6. Forward modules

Forward modules are used to trigger forward inference. Take for example the forward rule

  (#$implies
    (#$isa ?PRED #$BinaryPredicate)
    (#$arity ?PRED 2))

If someone creates a new predicate #$foo and asserts

  (#$isa #$foo #$BinaryPredicate)

then forward inference can be triggered by indexing alone. But what if instead you assert

  (#$isa #$foo #$TransitiveBinaryPredicate)

?

Then some genls reasoning is needed to trigger the relevant forward rule. Forward modules take care of this kind of inference when determining which forward rules to trigger.

The different types of forward modules are:

11.3.6.a. transitiveViaArg forward modules

Forward modules to perform the above kinds of triggering for #$isa, #$genls, #$genlMt, #$genlPreds, #$genlInverse, #$genlAttributes, and the negations of each.

11.3.6.b. Symmetry and Asymmetry

There are forward modules for symmetry and asymmetry; given (p X Y), these conclude, respectively, (p Y X) and (not (p Y X)).

11.3.6.c. #$genlPreds and relata

There is another forward module for #$genlPreds:

If you asserted

  (p X Y)

and it is true that

  (genlPreds p q)

then one of the #$genlPreds forward modules would trigger a forward rule with an antecedent literal of the form

  (q X Y)

There are analogous forward modules for #$genlInverse, #$negationPreds, and #$negationInverse.

11.3.6.d. Evaluatable Functions

There is a forward module to inhibit forward inference on evaluatable functions.

11.3.6.e. termOfUnit

There is a forward module to handle forward inference for #$termOfUnit.