Reifiable Functions

#$ReifiableFunction   reifiable functions
    A specialization of #$Function-Denotational. Each instance of #$ReifiableFunction is denoted by a CycL constant that can stand in the 0th (or arg0 ) position in a #$CycLReifiableNonAtomicTerm (q.v.). For example, #$GovernmentFn is a reifiable function, so the term `(#$GovernmentFn #$France)' is a reifiable non-atomic term (or NAT ). And since this particular term actually _is_ reified in the Cyc Knowledge Base, it is, more specifically, a #$CycLNonAtomicReifiedTerm (or NART ). The NART `(#$GovernmentFn #$France)' is treated more or less the same as if it were a CycL constant (named, say, `GovernmentOfFrance'). Similary, the constant for #$GovernmentFn can be applied to the constant (or other reified or reifiable term) for _any_ instance of #$GeopoliticalEntity to form a reifiable NAT that denotes that region's government; and should this NAT appear in a sentence that is asserted to the KB, it will thereby become a NART. Note, however, that not all NATs are such that it is desireable that they should become reified (i.e. become NARTs) if they appear in assertions; for more on this see #$UnreifiableFunction and #$CycLUnreifiedReifiableNonAtomicTerm.
    guid: bd588002-9c29-11b1-9dad-c379636f7270
    direct instance of: #$FunctionCategory #$AtemporalNecessarilyEssentialCollectionType
    direct specialization of: #$Function-Denotational 
    direct generalization of: #$DerivedWordFormingFunction #$SubcollectionRelationFunction-TypeLevel #$MetricUnitPrefix #$AnimalPartRegionFunction #$VariableAritySkolemFuncN #$SubcollectionRelationFunction-InstanceLevel #$SkolemFuncN #$VariableAritySkolemFunction #$SkolemFunction #$SubcollectionFunction #$SubcollectionRelationFunction-Inverse #$SubcollectionRelationFunction-Canonical #$UnaryIntersectionFunction

#$CycLReifiableDenotationalTerm   CycL reifiable denotational terms    **COMMENT NOT REVIEWED**    **GAFs NOT REVIEWED**

    A subcollection of both #$CycLClosedDenotationalTerm and #$CycLIndexedTerm (qq.v.). #$CycLReifiableDenotationalTerm is the collection of all CycL terms that both may be reified and may denote something in the universe of discourse. It thus includes all instances of #$CycLConstant as well as any NAT (see #$CycLNonAtomicTerm and #$Function-Denotational) whose functor denotes an instance of #$ReifiableFunction. For example, the NAT `(#$GovernmentFn #$France)' is a #$CycLReifiableDenotationalTerm, since #$GovernmentFn is an instance of #$ReifiableFunction. Similarly, `(#$JuvenileFn #$Platypus)' is a #$CycLReifiableDenotationalTerm; although it is not currently reified in the KB, it is reifiable and denotational (see #$CycLClosedDenotationalTerm). Finally, `(#$BorderBetweenFn #$Canada #$Mexico)' is a #$CycLReifiableDenotationalTerm; although it happens not to denote anything in the universe of discourse, it is nonetheless the kind of NAT that can and often does denote. Note that #$CycLVariables are not considered reifiable terms.
    guid: bd63a0ce-9c29-11b1-9dad-c379636f7270
    direct instance of: #$AtemporalNecessarilyEssentialCollectionType #$CycLExpressionType
    direct specialization of:
    direct generalization of: #$ELReifiableDenotationalTerm #$HLReifiedDenotationalTerm #$CycLReifiableNonAtomicTerm #$CycLConstant #$CycLReifiedDenotationalTerm #$CognitiveCycFORT #$UMLFORT

#$termOfUnit   term of unit    **COMMENT NOT REVIEWED**    **GAFs NOT REVIEWED**

    #$termOfUnit is an inference-related Cyc predicate which appears in system-generated assertions; #$termOfUnit maps unreified reifiable non-atomic terms ( NATs -- see #$CycLUnreifiedReifiableNonAtomicTerm) to indexed data structures reified by the system. Assertions with #$termOfUnit are added by the system when an unreified reifiable NAT first appears in a Cyc formula that is added to the knowledge base. When such a NAT is first used in a formula, the Cyc system automatically creates an indexed data structure to reify the NAT. A name is automatically assigned to the new data structure by the Cyc system. (Typically, it is a name which is identical to the unreified reifiable NAT, but one should not be misled by this identity into thinking that #$termOfUnit is a specialization of #$equals.) The predicate #$termOfUnit maps the system-generated data structure to the original NAT. (#$termOfUnit DATA-STRUCTURE NAT) means that the data structure DATA-STRUCTURE was created to reify the value of the non-atomic term NAT, and that NAT refers to DATA-STRUCTURE, which in turn denotes something in the range of the function in the 0th (or arg 0 ) position of NAT. For example, if an assertion such as (#$isa (#$RepairingFn #$Automobile) #$ProductType) introduced the unreified reifiable NAT (#$RepairingFn #$Automobile) in the Cyc knowledge base, the system would create a data structure to reify the value of (#$RepairingFn #$Automobile). The system would assign the name (#$RepairingFn #$Automobile) to the newly created data structure. The system would also associate the newly reified data structure with the unreified refiable NAT by means of the #$termOfUnit assertion, (#$termOfUnit (#$RepairingFn #$Automobile) (#$RepairingFn #$Automobile). Note: #$termOfUnit assertions are entered in the #$BaseKB because the mapping between a NAT and the data structure reified for it holds universally. One should view #$termOfUnit assertions as bits of bookkeeping knowledge which are very rarely, if ever, entered into the Cyc knowledge base by hand.
    guid: bd5880e4-9c29-11b1-9dad-c379636f7270
    direct instance of: #$ReformulatorIrrelevantFORT #$InferenceRelatedBookkeepingPredicate #$StrictlyFunctionalPredicate #$DefaultMonotonicPredicate #$BinaryPredicate

#$SkolemFunction   skolem function    **COMMENT NOT REVIEWED**    **GAFs NOT REVIEWED**

    #$SkolemFunction is a collection of Cyc system-generated functions that implement existential quantifications in Cyc. Whenever someone asserts to Cyc an expression that contains a `#$thereExists', Cyc automatically creates a new instance of #$SkolemFunction and rewrites the assertion using that Skolem function, as described in what follows. (Most Cyc users don't need to know the following details, which are supplied only for the curious.) Suppose we tell Cyc that every animal has a birth date; i.e., for each animal, there exists a date such that the animal was born on that date --- in CycL, (#$implies (#$isa ?X #$Animal)(#$thereExists ?Y (#$birthDate ?X ?Y))). In response to that CycL formula, Cyc would create a new element of #$SkolemFunction -- we might call it the `BirthDateFn' -- whose single argument would be an animal and whose resultant value would be a date, namely, that animal's date of birth. Subsequently, Cyc would automatically use the `BirthDateFn' in asserting our rule, eliminating the need for a `#$thereExists'. Our formula would thus be rewritten by the system, as follows: (#$implies (#$and (#$isa ?X #$Animal) (#$termOfUnit ?Y (`BirthDateFn' ?X))) (#$birthDate ?X ?Y)). See also #$termOfUnit. Note: Although our example uses the name 'BirthDateFn' for our Skolem function, at this time (4/97), Skolem functions are automatically named by the Cyc system using the prefix `SKF-' followed by a number.
    guid: c05813b7-9c29-11b1-9dad-c379636f7270
    direct instance of: #$AtemporalNecessarilyEssentialCollectionType #$FunctionCategory
    direct specialization of: #$ReifiableFunction 
    direct generalization of: #$VariableAritySkolemFunction #$FixedAritySkolemFunction #$SkolemFuncN