MELD features
[Cyc Logo] Features of MELD
E-Mail Comments to: doc@cyc.com Version 0.3 Last Update: February 25, 1998 Copyright© 1997, 1998 Cycorp All rights reserved. Cyc® is a Registered Trademark of Cycorp, Inc.
This document describes some of the more important features of the Moderately Expressive Logical Description (MELD). A formal BNF will be found in Appendix C, below, but we believe that most prospective users of this language -- for now, that means HPKB participants and Cycorp customers -- will find a tutorial document such as this one of more use than that appendix.
MELD is a formal language whose syntax derives from first-order predicate calculus (the language of formal logic). In order to express real-world expertise and even just plain old common sense knowledge, however, it goes far beyond first order logic. The vocabulary of MELD consists of terms: semantic constants, non-atomic terms (NATs), variables, numbers, strings, etc. Terms are combined into meaningful MELD expressions, ultimately forming meaningful closed MELD sentences (with no free variables.) A set of MELD sentences forms a knowledge base. In this document, for example, we will refer to the IKB, which is the DARPA HPKB Integrated Knowledge Base, and we will refer to the Cyc KB, which is a much larger MELD knowledge base.
The topmost (most general) content of the IKB and also of the Cyc KB -- certain abstract terms and the fundamental axioms interrelating and using those terms -- forms the kernel of every MELD knowledge base. In fact, the semantics of MELD require and assume the existence of those terms, axioms, etc. (for example, collections such as #$Thing and #$Collection and #$Predicate, predicates such as #$isa and #$arg2Isa, and axioms such as the fact that the #$arg2Isa of #$isa is #$Collection.) Those terms (about 160 of them) and assertions (about 650 of them) are part of the definition of MELD, and are listed in this document as Appendix A.
Every MELD implementation is likely to make some choices, and add some special purpose code, for efficiency's sake. MELD is a purely declarative language, hence those issues are orthogonal (or meta-) to the specification of MELD. However, as a help to real flesh and blood MELD users and implementors, we've collected some of the most important main remarks about this topic as Appendix B.
Contents
- 1 Contents:
- 1.1 Constants
- 1.2 Variables
- 1.3 Formulas
- 1.4 Predicates
- 1.5 Logical Connectives
- 1.6 Complex Formulas
- 1.7 Well-Formedness of Quantified Formulas
- 1.8 Alternate logic reasoning systems
- 1.8.1 Probabilities, including Bayesian (Pearlian) nets
- 1.8.1.1 Stating Prior and Derived Probabilities
- 1.8.1.2 Calculating Prior and Derived Probabilities
- 1.8.1.3 Weak Constraints
- 1.8.1.4 Second-Order and Higher-Order probabilities
- 1.8.1.5 Relative Probability
- 1.8.1.6 Single Dependency Conditional Probability
- 1.8.1.7 Multiple Dependency Conditional Probability
- 1.8.1.8 Bayes Nets
- 1.8.1.9 Constraints on Probability Systems
- 1.8.2 Fuzzy Sets & Truth Values
- 1.8.3 Supports
- 1.8.1 Probabilities, including Bayesian (Pearlian) nets
- 2 Appendix A: Formulas true in every MELD KB
- 2.1 ;;; #$AntiSymmetricBinaryPredicate
- 2.2 ;;; #$Assertion
- 2.3 ;;; #$AsymmetricBinaryPredicate
- 2.4 ;;; #$AttributeValue
- 2.5 ;;; #$BaseKB
- 2.6 ;;; #$BinaryPredicate
- 2.7 ;;; #$BookkeepingMt
- 2.8 ;;; #$BookkeepingPredicate
- 2.9 ;;; #$BroadMicrotheory
- 2.10 ;;; #$Collection
- 2.11 ;;; #$CollectionDenotingFunction
- 2.12 ;;; #$CommutativeRelation
- 2.13 ;;; #$CycELVariable
- 2.14 ;;; #$CycExpression
- 2.15 ;;; #$CycFormula
- 2.16 ;;; #$CycIndexedTerm
- 2.17 ;;; #$CycSystemList
- 2.18 ;;; #$CycSystemString
- 2.19 ;;; #$CycSystemSymbol
- 2.20 ;;; #$Cyclist
- 2.21 ;;; #$CyclistsMt
- 2.22 ;;; #$DefaultMonotonicPredicate
- 2.23 ;;; #$EvaluatableFunction
- 2.24 ;;; #$False
- 2.25 ;;; #$Format
- 2.26 ;;; #$ForwardInferencePSC
- 2.27 ;;; #$FunctionTheMathematicalType
- 2.28 ;;; #$Guest
- 2.29 ;;; #$HumanCyclist
- 2.30 ;;; #$IndividualObject
- 2.31 ;;; #$InferenceRelatedBookkeepingPredicate
- 2.32 ;;; #$Integer
- 2.33 ;;; #$IntervalEntry
- 2.34 ;;; #$IrreflexiveBinaryPredicate
- 2.35 ;;; #$ListTheFormat
- 2.36 ;;; #$Microtheory
- 2.37 ;;; #$NonNegativeInteger
- 2.38 ;;; #$NonPredicateFunction
- 2.39 ;;; #$PositiveInteger
- 2.40 ;;; #$Predicate
- 2.41 ;;; #$ProblemSolvingCntxt
- 2.42 ;;; #$QuaternaryPredicate
- 2.43 ;;; #$QuintaryPredicate
- 2.44 ;;; #$RealNumber
- 2.45 ;;; #$ReflexiveBinaryPredicate
- 2.46 ;;; #$ReifiableFunction
- 2.47 ;;; #$ReifiableTerm
- 2.48 ;;; #$Relationship
- 2.49 ;;; #$Set-Mathematical
- 2.50 ;;; #$SetOrCollection
- 2.51 ;;; #$SetTheFormat
- 2.52 ;;; #$SiblingDisjointAttributeType
- 2.53 ;;; #$SiblingDisjointCollection
- 2.54 ;;; #$SingleEntry
- 2.55 ;;; #$SkolemFuncN
- 2.56 ;;; #$SkolemFunction
- 2.57 ;;; #$SubAbs
- 2.58 ;;; #$SymmetricBinaryPredicate
- 2.59 ;;; #$TemporalObject
- 2.60 ;;; #$TernaryPredicate
- 2.61 ;;; #$TheSet
- 2.62 ;;; #$TheTerm
- 2.63 ;;; #$Thing
- 2.64 ;;; #$TransitiveBinaryPredicate
- 2.65 ;;; #$True
- 2.66 ;;; #$UnaryPredicate
- 2.67 ;;; #$UnaryTypePredicate
- 2.68 ;;; #$VariableArityRelation
- 2.69 ;;; #$abnormal
- 2.70 ;;; #$afterAdding
- 2.71 ;;; #$afterRemoving
- 2.72 ;;; #$and
- 2.73 ;;; #$arg1Format
- 2.74 ;;; #$arg1Genl
- 2.75 ;;; #$arg1Isa
- 2.76 ;;; #$arg2Format
- 2.77 ;;; #$arg2Genl
- 2.78 ;;; #$arg2Isa
- 2.79 ;;; #$arg3Format
- 2.80 ;;; #$arg3Genl
- 2.81 ;;; #$arg3Isa
- 2.82 ;;; #$arg4Format
- 2.83 ;;; #$arg4Genl
- 2.84 ;;; #$arg4Isa
- 2.85 ;;; #$arg5Format
- 2.86 ;;; #$arg5Genl
- 2.87 ;;; #$arg5Isa
- 2.88 ;;; #$argsGenl
- 2.89 ;;; #$argsIsa
- 2.90 ;;; #$arity
- 2.91 ;;; #$coExtensional
- 2.92 ;;; #$comment
- 2.93 ;;; #$cyclistNotes
- 2.94 ;;; #$defnIff
- 2.95 ;;; #$defnNecessary
- 2.96 ;;; #$defnSufficient
- 2.97 ;;; #$different
- 2.98 ;;; #$disjointWith
- 2.99 ;;; #$elementOf
- 2.100 ;;; #$equals
- 2.101 ;;; #$exceptFor
- 2.102 ;;; #$exceptWhen
- 2.103 ;;; #$forAll
- 2.104 ;;; #$genlAttributes
- 2.105 ;;; #$genlInverse
- 2.106 ;;; #$genlMt
- 2.107 ;;; #$genlPreds
- 2.108 ;;; #$genls
- 2.109 ;;; #$hasAttributes
- 2.110 ;;; #$holdsIn
- 2.111 ;;; #$implies
- 2.112 ;;; #$interArgIsa1-2
- 2.113 ;;; #$interArgIsa1-3
- 2.114 ;;; #$interArgIsa1-4
- 2.115 ;;; #$interArgIsa1-5
- 2.116 ;;; #$interArgIsa2-1
- 2.117 ;;; #$interArgIsa2-3
- 2.118 ;;; #$interArgIsa2-4
- 2.119 ;;; #$interArgIsa2-5
- 2.120 ;;; #$interArgIsa3-1
- 2.121 ;;; #$interArgIsa3-2
- 2.122 ;;; #$interArgIsa3-4
- 2.123 ;;; #$interArgIsa3-5
- 2.124 ;;; #$interArgIsa4-1
- 2.125 ;;; #$interArgIsa4-2
- 2.126 ;;; #$interArgIsa4-3
- 2.127 ;;; #$interArgIsa4-5
- 2.128 ;;; #$interArgIsa5-1
- 2.129 ;;; #$interArgIsa5-2
- 2.130 ;;; #$interArgIsa5-3
- 2.131 ;;; #$interArgIsa5-4
- 2.132 ;;; #$relationExistsAll
- 2.133 ;;; #$relationExistsCountAll
- 2.134 ;;; #$isa
- 2.135 ;;; #$ist
- 2.136 ;;; #$lispDefun
- 2.137 ;;; #$minimizeExtent
- 2.138 ;;; #$mtInferenceFunction
- 2.139 ;;; #$myCreationTime
- 2.140 ;;; #$myCreator
- 2.141 ;;; #$negationAttribute
- 2.142 ;;; #$negationInverse
- 2.143 ;;; #$negationPreds
- 2.144 ;;; #$not
- 2.145 ;;; #$oldConstantName
- 2.146 ;;; #$or
- 2.147 ;;; #$relationAllExists
- 2.148 ;;; #$relationAllExistsCount
- 2.149 ;;; #$requiredArg1Pred
- 2.150 ;;; #$requiredArg2Pred
- 2.151 ;;; #$resultgenl
- 2.152 ;;; #$resultIsa
- 2.153 ;;; #$satisfiesDescription
- 2.154 ;;; #$siblingDisjointExceptions
- 2.155 ;;; #$termOfUnit
- 2.156 ;;; #$thereExistAtLeast
- 2.157 ;;; #$thereExistAtMost
- 2.158 ;;; #$thereExistExactly
- 2.159 ;;; #$thereExists
- 3 Appendix B: Remarks about MELD Implementations
- 4 Appendix C: BNF Grammar for MELD
Contents:
- Constants
- Constant Names
- Variables
- Formulas
- Predicates
- Predicate Arity
- Predicate Argument Types
- Logical Connectives
- not
- and
- or
- xor
- implies
- equivalent
- Complex Formulas
- Quantification
- forAll
- Multiple Quantification
- Unbound Variables
- thereExists
- thereExistExactly, thereExistAtLeast, thereExistAtMost
- Second-order Quantification
- Well-Formedness of Quantified Formulas
- Non-Atomic Terms
- Functions
- Function Arity
- Function Argument Types and Result Types
- Individual Denoting Functions vs. Collection Denoting Functions
- Microtheories
- Truth Values
- Probabilities
- Fuzzy Sets and Truth Values
- Supports
- Appendix A: Formulas true in every MELD KB
- Appendix B: Remarks about MELD Implementations
- Constant-Naming Strategies
- Variable-Naming Strategies
- Conventions for permitting/repairing unbound variables in formulas
- Assertions
- Directions
- Canonicalization of Assertions
- Skolemization
- Reifiable vs. Non-Reifiable Functions
- Quantifying into NATs
- Appendix C: BNF Grammar for MELD
- Footnotes
Constants
Constants are the "vocabulary words" of the MELD language; more precisely, they are the "words" that are used in writing the axioms (i.e., the closed formulas) that comprise the content of any MELD knowledge base, such as the Cyc KB or the IKB or the MELD KERNEL KB. Most useful knowledge based systems (not just MELD KBs) attempt to model the world as most sane, adult humans perceive it, with each constant representing some thing or concept in the world that (some group of) people know about and/or could understand. For those of you familiar with the Cyc system, you can think of IKB as the upper and middle parts of Cyc's ontology and content, and think of the MELD KERNEL KB as the common uppermost part of both of those ontologies and content.
Each MELD KB contains constants that denote collections of other concepts, such as #$Typewriter (the collection of all typewriters) and #$Walking (the collection of all actions in which some animal walks). Each MELD KB also contains constants that denote individual non-collection things, some of which are more-or-less permanently in that KB, like #$InternalRevenueService and #$Canada and #$BillClinton, and some of which might get created only when reasoning about some state of affairs, like #$Walking00036 (a particular case of walking), and might be ephemeral, getting deleted after some question is answered or some session is over.
Some of the constants represented in a MELD KB are predicates, such as #$isa or #$likesAsFriend, that enable you to express relationships among other constants. Some other constants are functions, such as #$GovernmentFn and #$MotherFn, which can take constants (collections and/or non-collections) or other things as arguments, and generate new concepts. For example, the expression (#$GovenmentFn #$Canada) represents the government of Canada, and the expression (#$MotherFn #$BillClinton) represents Bill Clinton's mother. Note that these full expressions (functions applied to their arguments) are not themselves individuals -- or for that matter even constants -- but each of their constituent parts is, and so is their value. Such expressions are called non-atomic terms (NATs). Other kinds of non-constant terms include lists, numbers, characters, and strings.
The meaning of a constant is the totality of the set of sentences in the KB involving that constant. Part of this definition is locally asserted (e.g., by a human knowledge enterer) and part of it is inferred (by some inference procedure) from the rest of the KB. Since inference won't in general be complete, that means that almost all the time we're forced to deal with partial definitions of terms, Only rarely can we precisely, completely define anything. This is perhaps not so different from what we as humans are forced to put up with in our daily lives in the real world. (see Footnote)
Constant Names
MELD constants must have unique names, such as #$MaryShepherd439, #$massOfObject, or #$MapleTree.
Constant names can include any uppercase or lowercase letter (from A to Z), any digit (from 0 to 9), and the symbols "-" (a hyphen), "_" (an underscore), and "?" (a question mark). No other special characters, such as "!", "&", or "@" are allowed. Let alone things like backspaces. (Footnote)
MELD constant names are case-sensitive. #$BillClinton will always be referred to exactly in that form. And it is not the same constant name as BILLCLINTON or billclinton.
Remember that the names we assign to constants mean nothing to MELD. It doesn't matter whether the concept green is called Green, GreenColor, Verde, Gruen, or EMRG. The names are just scaffolding. It is the set of sentences in the KB that mention that constant -- axioms we've provided, conclusions inferred by the system, etc. -- that impart meaning to the symbol. Of course scaffolding for buildings in real life is useful, and so too having mnemonic names for constants in MELD is also useful. A good analogy is choosing a web site; it's better for IBM to choose ibm.com than to choose intl-bus-mchn-corp.com or mnbvcxzlkjhgfpoiuytrew.com.
Conversely, it is also very important never to assume that you, the human observer of a MELD KB, can know with certainty what a constant denotes to the system, just from seeing its name and nothing else. For example, "Function" is a bad name to choose, but if someone has chosen it then you must examine the assertions about it, or at least its place in the ontological hierarchy, to determine whether it is meant to represent mathematical functions, physiological functions, roles in a company, the English word function, etc.
To reiterate this point: For convenience, we usually select nice mnemonic names for MELD constants, but until/unless we also assert sentences about the constants into the KB, MELD can't distinguish CENSORED.
Variables
Quantified MELD expressions (discussed below) contain one or more variables which stand for terms (e.g., constants) or formulas whose identities are not specified.
A variable may appear anywhere that a term or formula can appear. Variable names must begin with a question mark ("?") and may be of any length. Having a special prefix character like this is necessary to distinguish them from MELD constants. E.g., the variable ?UN versus the MELD constant UN. Variable names are not case-sensitive; that is, ?per and ?PER are the same variable.
After the question mark comes an alphabetic character (A-Z), followed by any number of alphanumeric characters, hyphens, and underscores.
Formulas
MELD formulas combine terms into meaningful expressions.
Every MELD formula has the structure of a parenthesized list. That is, it starts with a left parenthesis, then there follow a series of objects which are commonly designated ARG0, ARG1, ARG2, etc., and finally there is a matching right parenthesis. The object in the ARG0 position may be a predicate, a logical connective, or a quantifier. The remaining arguments may be terms (e.g., constants, non-atomic terms, variables, numbers, strings delimited by double quotes ("...")), or other formulas. Note the recursion here; ARG4 in one formula might itself be an entire MELD formula.
#$MELDFormula represents the class of well-formed MELD formulas. If a MELD formula satisfies all the constraints on the number and types of arguments to the relations/predicates/quantifiers/. . . that appear in it, then it is considered an instance of the class #$MELDFormula.
The simplest kind of formula is a formula in which the ARG0 position is occupied by a predicate, and all the other argument positions are filled with terms (or variables):
(#$likesAsFriend #$DougLenat #$KeithGoolsbey)
(#$skillCapableOf #$LinusVanPelt #$PlayingAMusicalInstrument #$performedBy)
(#$colorOfObject ?CAR ?COLOR]])
The first two of the simple formulas above are called ground atomic formulas (GAFs), since none of the terms filling the argument positions ARG0, ARG1, ARG2, etc. are variables. The third formula is not a GAF; it refers to the variables ?CAR and ?COLOR. We will discuss more complicated sorts of formulas later in this document.
Predicates
Every MELD atomic formula must begin with a predicate or a variable in order to be well-formed.
Predicate Arity
Most predicates are defined to take a fixed number of arguments. There are no optional predicate arguments in MELD. However, a few predicates, such as #$different, can take a variable number of arguments. Such predicates are elements of the collection #$VariableArityRelation. New instances of that class -- say #$mutuallyFarApart -- may be defined simply by asserting the formula (#$isa #$mutuallyFarApart #$VariableArityRelation) into the KB.
The number of arguments a predicate takes is determined by its #$arity. A #$predicate is described as 0-ary, unary, binary, ternary, quaternary, quinary, etc., according to whether it takes 0, 1, 2, 3, 4, 5, etc. arguments. There's no limit to the arity, but most predicates are binary or unary; most of the rest are ternary; most of the rest are quaternary; etc. In the entire Cyc KB, e.g., no predicate has needed to be defined that takes more than 5 arguments.
To be well-formed, an atomic formula must have the right number of arguments for the predicate filling the ARG0 position. So, e.g.,
(#$isa #$DougLenat #$Person #$AustinThing)
is not well-formed, since the arity of isa is 2, but this formula gives it 3 arguments.
The arity of a predicate is a semantic constraint imposed by making an assertion to the KB, in MELD, of the form ( #$#$arity #$likesAsFriend 2), (#$arity #$between 3), etc. The (#$#$arity . . . ) assertions for the predicates which are part of the MELD KERNEL KB are also all a part of that KERNEL KB; see Appendix B.
For example, (#$arity #$isa 2). Since arity is itself one of those predicates, there is an assertion about the arity of arity, namely (#$arity #$arity 2).
Predicate Argument Types
The "type" of each argument of each predicate must be specified; that is, the appropriate formulas must be asserted to be true in the KB. These assertions use the predicates #$arg1Isa, #$arg2Isa, etc. which mean "argument _<n>_ is an instance of _<collection>_". For example, the #$arg1Isa of #$likesAsFriend is #$Person, meaning that only people like each other as friends in this exact sense. Presumably there are other predicates to express two countries being allies, two dogs that get along well together, etc. As another example, #$arg2Isa of #$arg2Isa itself is #$Collection, since the "type" of an argument is specified by naming a collection (such as #$Person, #$ShelterConstruction, #$Predicate,. . .) There must be (and are) formulas in the MELD KERNEL KB that assert that the first argument to #$arity is a predicate (or function) and the second argument is a non-negative integer. As another example, suppose the predicate #$residesInDwelling is partially defined by asserting the following axioms into the KB:
(#$isa #$residesInDwelling #$BinaryPredicate) (#$arg1Isa #$residesInDwelling #$Animal) (#$arg2Isa #$residesInDwelling #$ShelterConstruction)
To be well-formed, every formula which has #$residesInDwelling in the ARG0 position must have a term which is an instance of #$Animal in the ARG1 position, and a term which is an instance of #$ShelterConstruction in the ARG2 position.
So the formula
( #$residesInDwelling #$PottedPlant37 #$KarensHouse)
is probably not well-formed.
Though we can never be absolutely certain just from the names, #$KarensHouse probably is an instance of #$ShelterConstruction, but #$PottedPlant37 is probably not an instance of #$Animal.
The arguments of some predicates actually are themselves collections (in addition to of course their each being an instance of some collections as usual).
In this case an additional form of type-constraint is available: #$arg1Genl, #$arg2Genl, etc. (meaning "argument <n>_ has generalization _<collection>_")
For example,
(#$isa #$presentationMediumFor #$BinaryPredicate ) (#$arg1Isa #$presentationMediumFor #$ExistingObjectType ) (#$arg1Genl #$presentationMediumFor #$InformationBearingObject ) (#$arg2Isa #$presentationMediumFor #$Collection ) (#$arg2Genl #$presentationMediumFor #$PropositionalInformationThing )
means that the two arguments of the predicate #$presentationMediumFor are collections, and that the first collection has the collection #$InformationBearingObject as a #$generalization (i.e., as a superset), and that the second collection has #$PropositionalInformationThing as a #$generalization.
Thus the assertion
(#$presentationMediumFor #$Blueprint #$ArchitecturalDesign )
is syntactically well-formed and relates the collection of all blueprints and the collection of all architectural designs;
to check that the formula is semantically well-formed, MELD would
- determine the #$arity of #$presentationMediumFor (it would infer (#$arity #$presentationMediumFor 2 ) from the (#$isa #$presentationMediumFor #$BinaryPredicate) assertion),
- check that the formula indeed has the right number of arguments, in this case 2, and
- check that the collection #$Blueprint is known (again modulo inference) to be a subclass of #$InformationBearingObject, and
- check that the collection #$ArchitecturalDesign similarly has, as one of its generalizations, the collection #$PropositionalInformationThing.
Note that the KB is required to do this semantic well-formedness checking of formulas.
Another type of constraint on (or, if you prefer, partial definition of) a predicate involves inter-argument constraints; these are expressed in MELD by a family of predicates analogous to #$arg1Isa,. . . above.
Here are two simple examples:
(#$interArgIsa1-2 #$mother ?x (#$FemaleFn ?x) ) (#$interArgIsa1-2 #$mother ?x (#$AdultFn ?x) )
This says that if the first argument of (#$mother a b) is an instance of #$Person, then the second argument must be an instance of (#$FemaleFn #$Person), and also must be an instance of (#$AdultFn #$Person), that is, an adult female person.
In practice, as an efficiency issue, it would be more common to assert just those inter-argument constraints that will actually come up frequently,
such as
( #$interArgIsa1-2 #$mother #$Person #$FemalePerson )
etc.
Logical Connectives
More complex formulas can be built up out of atomic formulas (and/or other complex formulas) by using logical connectives, which are special constants analogous to the logical operators of formal logic. The most important logical connectives in MELD are: and, or, not. Also important are the connectives xor, implies, equivalent . New connectives (e.g., shefferStroke) can be introduced simply by asserting a formula to that effect into the KB; thus (#$isa #$shefferStroke #$Connective). To be defined, though, there should be additional formulas that specify how many arguments the connective takes, and what its definition is in terms of other connectives such as #$and/#$or/#$not. The type of each argument that each connective takes is always #$MELDFormula, meaning a well-formed MELD formula.
#$not
This connective takes a single MELD formula as an argument. Like the "not" of formal logic, it reverses the truth value of its argument.
Thus,
(#$not (#$colorOfObject #$FredsBike #$RedColor) )
will be true if and only if
(#$colorOfObject #$FredsBike #$RedColor)
is false.
Likewise,
(#$not (#$not (#$colorOfObject #$FredsBike #$RedColor ) ) )
will have the same truth value as
(#$colorOfObject #$FredsBike #$RedColor).
#$and
This connective takes zero or more formulas as arguments. Like the "and" of formal logic, it returns true if and only if each of its arguments evaluates to true.
Here's an example:
(#$and (#$colorOfObject #$FredsBike #$RedColor ) (#$objectFoundInLocation #$FredsBike #$FredsGarage ) )
This formula states that Fred's bike is red and that it is located in Fred's garage. If both of those things are true then the whole formula is true, but if one or both are false, then the whole formula is false.
As we have said before, MELD is a declarative language; the order of evaluation/examination of conjuncts does not matter; it can and will be chosen by the MELD implementation, however it wishes to do so, so as to make things as efficient as possible; therefore, one should not write assertions that in any way rely on the order in which one states a series of conjuncts.
For completeness, and following mathematical custom, if this connective is applied to zero arguments then its value is taken to be #$True.
#$or
The connective or takes zero or more formulas as arguments. Like the "inclusive or" of formal logic, it returns true if and only if at least one of its arguments evaluates to true.
Here's an example:
(#$or (#$colorOfObject #$FredsBike #$RedColor ) (#$objectFoundInLocation #$FredsBike #$FredsGarage ) (#$owns #$Fred #$FredsBike ) )
This assertion states that either Fred's bike is red, or it is located in Fred's garage, or Fred owns it. If any one, or any two, or all of these three statements is/are true, then the whole formula is true. All three formulas would have to be false for the disjunction -- the formula as a whole -- to be false. The order of evaluation/examination of disjuncts does not matter and should never be relied on in any way by the formula-writers.
For completeness, and following mathematical custom, if this connective is applied to zero arguments then its value is taken to be #$False.
#$xor
The connective xor takes precisely two formulas as arguments. Like the binary "exclusive or" of formal logic, it returns true if and only if precisely one of its arguments evaluate to true. Here's an example:
(#$xor ( #$colorOfObject #$FredsBike #$RedColor ) ( #$objectFoundInLocation #$FredsBike #$FredsGarage ) )
This assertion states that either Fred's bike is red, or it is located in Fred's garage but not both. If only one of these statements is true, and the other false, then the whole formula is true. If both are false or both are true, the formula as a whole would be false. This connective is defined in terms of the others, above. One can also define a form of exclusive or that takes 3, 4, or any number of formulas as arguments. This connective is defined in terms of the others, above. I.e., MELD supports the dynamic declarative definition of new logical connectives in terms of the base connectives (and/or/not) as follows:
(#$logicalConnectiveExpansion <connective> <connective use> <expanded equivalent>)
To define #$xor, the pertinent formula to assert is:
( #$logicalConnectiveExpansion #$xor ( #$xor ?ARG1 ?ARG2 ) ( #$or (#$and ?ARG1 ( #$not ?ARG2 ) ) (#$and ( #$not ?ARG1 ) ?ARG2 ) ) )
Of course one also must assert formulas that state that #$xor is a logical connective, that its arity is 2, etc.
Note that #$logicalConnectiveExpansion quotes its arguments, and in effect is more like a very special sort of quantifier than it is like a predicate.
#$implies
This connective takes exactly two formulas as arguments. Like the "if-then" statement of formal logic, it returns true if and only if it is not the case that its first argument is true and its second argument is false.
Here's an example:
(#$implies (#$ownerOfObject #$Bike001 #$Fred) (#$colorOfObject #$Bike001 #$RedColor) )
This assertion states that if Bike001 is owned by Fred, then it is red. Newcomers to formal logic may misinterpret implies as implying a causal relationship. It doesn't. An (#$implies f1 f2) assertion says only that either the first argument f1 is false, or else the second argument f2 is true.
So, for example, the assertion
(#$implies (#$isa #$RichardNixon #$Country) (#$colorOfObject #$DougLenat #$PastelMintGreen) )
is quite true, because the first argument is false.
This connective is defined in terms of #$and/#$or/#$not, similarly to the way #$xor was defined, above.
Note that this connective takes exactly 2 arguments, and of course their order matters quite a bit. However, one cannot distinguish ('#$implies formula1 formula2) from logically equivalent formulas such as (#$implies (#$not formula2) (#$not formula1)'). Indeed, this connective is defined in terms of earlier ones (#$and/#$or/#$not).
Assertions involving implies are very common in MELD knowledge bases (including the Cyc KB and the HPKB IKB and, as shown in Appendix A below, even in the tiny MELD KERNEL KB). We also call these sorts of formulas "conditionals" or "rules", and we often refer to the first argument as the "antecedent" or "if-part" and the second argument as the "consequent" or "then-part".
Note, however, that the particular formulas above are so simple, and involve so few variables, that they are not representative of assertions likely to be found in Cyc or in the IKB or in the MELD KERNEL KB. We will come to some more representative examples in a moment.
#$equivalent
The connective "#$equivalent" takes precisely two formulas as arguments. Like the "if-and-only-if" (or "iff") statement of formal logic, (#$equivalent f1 f2) is true if and only if both arguments have the same truth value: that is, if both f1 and f2 are true or both f1 and f2 are false; otherwise (#$equivalent f1 f2) is false. Here's an example:
(#$equivalent (#$ownerOfObject #$Bike001 #$Fred) (#$colorOfObject #$Bike001 #$RedColor) )
This assertion states that if #$Bike001 is owned by #$Fred, then it is red; and if Bike001 is red, then it is owned by Fred. Newcomers to formal logic may misinterpret the logical connective "equivalent" as implying a semantic or even a co-occurrence equivalence. It doesn't entail any such thing. There may be no meaningful semantic connection between statements A and B, but if they share the same truth value then they stand in the relationship "equivalent" to each other. Thus the assertion
(#$equivalent ( #$isa #$RichardNixon #$Orange-TheFruit ) ( #$colorOfObject #$NewYorkCity #$PastelMintGreen ) )
is true, because both arguments are false.
Assertions involving "equivalent" are also called biconditionals or bidirectional rules; in mathematics, this is often denoted iff (for "if and only if").
This connective was defined in terms of #$and/#$or/#$not.
Note that the particular formulas above are not representative of equivalent assertions likely to be found in any real MELD KB; e.g., they don't involve any quantified variables, nested formulas as arguments, etc. We will come to some more representative examples in a moment.
Complex Formulas
One can compose the above connectives, of course, and have complex expressions such as (#$and . . . (#$or . . . (#$xor A (#$and . . . )'). . .'). . .)
The writer of a conjunction (disjunction, etc.) must not assume that the order of conjuncts (disjuncts, etc.) has any meaning whatsoever. Any MELD implementation is free to reorder the arguments of symmetric relations (including #$and, #$or, #$xor, #$equivalent; #$PlusFn, #$sibling,. . .) and to canonicalize complex formulas (e.g., break up a long formula into several shorter and simpler ones, etc.) -- for efficiency -- so long as the transformation preserves logical equivalence.
Even in the case of asymmetric relations such as #$implies, a MELD implementation may elect to transform or break up complex formulas involving it into simpler ones which, taken together, are logically equivalent to the original big formula.
Any complex formula formed by using the logical connectives will be well-formed if the formulas given as arguments to the connectives are also well-formed and if the right number of arguments is/are given. (The formulas given as arguments to the logical connectives need not be atomic formulas, like most of the examples above, but can be any well-formed formula.)
Another way of saying this is that #$not, #$and, #$or, #$xor, #$implies, and #$equivalent -- and any other instances of #$Connective that you define -- produce #$MELDFormulas when they are given (the correct number of) arguments which are also #$MELDFormulas.
Suppose A, B and C are syntactically legal, and D is not. Then,
(#$not A ) (#$and A ) (#$and A B ) (#$and A B C ) (#$or A ) (#$or A B ) (#$or A B C ) (#$and A A A A A A A A A B ) (#$xor A B ) (#$implies A B ) (#$equivalent A B )
would all be MELDFormulas. But
(#$not A B) (#$xor) (#$equivalent A B C) (#$and A D) (#$implies A)
would not be #$MELDFormulas.
Why? The first of these, (#$not A B), violates the requirement that the "not" connective takes only one formula as an argument.
The expressions (#$xor), (#$implies A) and (#$equivalent A B C) also violate restrictions on the number of formulas these connectives take as arguments.
(#$and A D) is not well-formed because D is not well-formed; any other formula that contained D would be syntactically bad for the same reason.
Quantification
So far, we have only looked at ways to make statements about specific objects, like #$FredsBike and #$RedColor and #$Canada. But MELD, like first-order predicate calculus, also gives us two (families of) ways to talk about objects without being specific about the identity of the objects involved: universal quantification and existential quantification. Universal quantification corresponds to English expressions like every, all, always, everyone, and anything, while existential quantification corresponds to English expressions like someone, something, and somewhere. MELD contains one universal quantifier, #$forAll, and four existential quantifiers, #$thereExists, #$thereExistAtLeast, #$thereExistAtMost, and #$thereExistExactly. One can introduce additional quantifiers, by making the appropriate assertions -- declaring the new quantifier to be an instance of #$Quantifier, and giving a "definition" of it, probably in terms of existing quantifiers, predicates, and collections.
#$forAll
The universal quantifier #$forAll takes two arguments: a variable and a formula in which (presumably!) that variable appears. In practice, the formula is often a conditional (#$implies . . .) in which the antecedent is used to restrict the scope of the variable. Here's an example:
(#$forAll ?X (#$implies (#$owns #$Fred ?X ) (#$objectFoundInLocation ?X #$FredsHouse ) ) )
This formula states that if Fred owns any object ?X, then that object is located in FredsHouse. In other words, all Fred's stuff is in his house. Note that this rule is of course only true by default; we will discuss this in a later section, below. Note also that we would not want to state a rule like this for entry into any "real" MELD KB; rather, we'd want a more general rule that applied to all people, not just Fred:
(#$forAll ?X (#$forAll ?H (#$forAll ?PER (#$implies (#$and (#$isa ?H #$House ) (#$residesAt ?PER ?H ) (owns ?PER ?X ) ) ( #$objectFoundInLocation ?X ?H ) ) ) ) )
In other words, most people keep most of the things they own at their place of residence -- at least by default. This is almost a good rule and is quite likely to be present in a broad MELD KB such as the Cyc KB or the HPKB IKB. It is representative of the rules which can, should, and have been made part of those MELD KBs.
Multiple Quantification
Formulas may contain more than one quantifier, as seen in the last example, and as seen here in this one:
(#$forAll ?X (#$forAll ?Y (#$implies (#$and ( #$owns #$Fred ?X) ( #$owns #$Fred ?Y) ) (#$near ?X ?Y) ) ) )
which says that any two things owned by Fred are near each other. Note that each quantifier introduces a new variable, and that each variable must have a different name from others bound in that same scope. Other rules can of course reuse the variables ?X, ?Y, ?PER, ?H,. . .
Unbound Variables
To be considered a closed sentence -- a well-formed formula -- all the variables in an expression need to be introduced ("bound") by a quantifier before they are used. Each quantifier binds exactly one variable, and every variable used should be bound by exactly one quantifier.
Furthermore, a variable has no meaning outside the scope of the quantifier which binds it.
Most MELD implementations will elect to treat unbound variables as universally quantified, but that is a feature of those implementations, and/or of the interface tools which users are employing to interact with the MELD KB and inference engine.
This is not a part of the MELD language itself.
For more information about this, see Conventions for permitting/repairing unbound variables in formulas in Appendix B.
#$thereExists
The existential quantifier #$thereExists takes two arguments: a variable and a formula in which that variable appears. In practice one typically uses #$thereExists only in a few common ways, of which the following is a simple example:
(#$forAll ?A (#$implies (#$isa ?A #$Animal ) (#$thereExists ?M (#$mother ?A ?M ) ) ) )
This assertion states that, for every animal, there exists at least one object which is that animal's mother. The object which is the animal's mother may be an object which is already represented by a MELD constant, or it may be a new object of which MELD has no knowledge. But unless and until it is told otherwise, MELD will assume that the object is a new one not necessarily identical with any "known" object.
#$thereExistExactly, #$thereExistAtLeast, #$thereExistAtMost
These three quantifiers are similar to #$thereExists, but provide greater quantitative expressiveness. Each of them takes three arguments: a positive integer, a variable, and a formula (in which the variable normally appears). Their meaning should be fairly self-explanatory.
Look at the following examples:
(#$forAll ?P (#$implies (#$isa ?P #$Person ) (#$thereExistExactly 2 ?LEG (#$and (#$isa ?LEG #$Leg ) (#$anatomicalParts ?P ?LEG ) ) ) ) )
(#$forAll ?T (#$implies (#$isa ?T #$Table ) (#$thereExistAtLeast 3 ?LEG (#$and (#$isa ?LEG #$Leg ) (#$anatomicalParts ?T ?LEG) ) ) ) )
(#$forAll ?P (#$implies (#$isa ?P #$Person) (#$thereExistAtMost 1 ?SPOUSE (#$spouse ?P ?SPOUSE ) ) ) )
Of course the truth of those statements is another matter altogether. Presumably each is true, at least by default, in some contexts; we will talk more about contexts below, in the section Microtheories.
Second-order Quantification
In the examples above, quantification took place over simple individuals or collections. However, quantification is also allowed over predicates, functions,arguments, and formulas.
For example:
(#$forAll ?S (#$implies (#$isa ?S #$KinshipFunction) (#$thereExists ?PRED2 (#$forAll ?X (#$forAll ?Y (#$equivalent (#$memberOfSet ?Y ( ?S ?X ) ) ( ?PRED2 ?X ?Y ) ) ) ) ) ) )
would be a perfectly valid use of quantification in MELD.
Here, the existentially quantified variable ?PRED2 ranges over all predicates, and the universally quantified variable ?S ranges over all functions but is constrained within the formula to be a #$Kinship function such as #$CousinFn.
Note that (?S ?X) denotes a set; if ?S is #$CousinFn then it denotes the set of cousins of ?X. Also note that they range over all possible predicates and functions, not just the ones that happen to be currently defined and named in the KB.
As mentioned above, a quantified variable may range over entire assertions, as in:
( #$forAll ?P ( #$implies ?P ( #$thereExists ... ) )
, over functions, and over arguments (justifications), as in ...
(#$thereExists ?J (#$and (#$justifies ?J ?P) (#$constructive ?J) ) )
... as well as ranging over predicates, collections, and individuals.
Well-Formedness of Quantified Formulas
As you probably by now expect, any formula (<quantifier> <variable> <formula>) or (<quantifier> <number> <variable> <formula>) beginning with a quantifier is well-formed if and only if its arguments are of the right number, of the right types, in the right order, and its <formula> argument is itself well-formed. This bottoms out in well-formedness of formulae which are predicates applied to arguments, and ultimately bottoms out in the well-formedness of individual terms, such as the variable ?PRED2 or the constant #$Canada. Note that this syntax technically allows the formula to make no mention of the bound variable, although most such assertions are useless.
Non-Atomic Terms
A non-atomic term (NAT) is a way of specifying a term using a function of some other term(s). Every ground NAT -- one which doesn't involve quantified variables -- is composed of nothing more or less than: a function and one or more arguments to that function. Consider, for example, the function #$FruitFn, which takes as an argument a type of plant and returns the collection of the fruits of that type of plant. This function can be used to build the following NATs:
(#$FruitFn #$AppleTree) (#$FruitFn #$PearTree) (#$FruitFn #$WatermelonPlant)
The expression (#$FruitFn #$AppleTree) has the same meaning as the constant term #$Apple, namely the set of all the apples, all the fruits of apple trees. Note that there may or may not already be a named MELD constant corresponding to the collection of apples (that is, a constant called #$Apple). The NAT (#$FruitFn #$AppleTree) provides a way of talking about this collection even if the corresponding constant does not exist. Similarly, they enable us to avoid having explicit terms like #$LiquidHydrogen, ... #$LiquidLawrencium, since those hundreds of terms can be expressed as NATs using the single function #$LiquidFn, as in (#$LiquidFn #$Oxygen) to denote the same term that #$LiquidOxygen would denote if it existed in the ontology, namely all portions (real or imagined, past or present or future, etc.) of liquid oxygen.
NATs can be used anywhere a constant can be used.
One could write, for example:
(#$implies ( #$isa ?APPLE ( #$FruitFn #$AppleTree) ) ( #$colorOfObject ?APPLE #$RedColor) ) or (#$filledWithStuffType (#$LOXTankFn #$SpaceShuttleChallenger ) (#$LiquidFn #$Oxygen) )
where #$LOXTankFn "returns" the liquid oxygen tank installed as part of that spacecraft. Notice that ?APPLE is a variable, and has nothing a priori to do with the constant #$Apple, or the constant #$APPLE, should such constants happen to exist in the ontology (vocabulary) of the MELD KB.
In order to build NATS, then, we need functions, not just predicates. This takes us to the next topic, therefore: MELD Functions.
Functions
Function Arity
Like most predicates, most functions have a fixed #$arity. A function is described as 0-ary, unary, binary, ternary, quaternary, quintary, etc. according to whether it takes 0, 1, 2, 3, 4, 5, etc. arguments. We are not aware of any useful MELD function currently defined that takes more than 5 arguments, but there is no limit to this in the language specification.
A few MELD functions do not have a fixed #$arity, but rather they can take a variable number of arguments. Mathematical functions like #$PlusFn are one example. One can give it any number of numbers, and its value is the sum of those numbers. New functions, of fixed and variable #$arity, are defined by simply making the appropriate assertions to the knowledge base, notably (#$isa <new function> #$Function), (#$arity <new function> 3) or whatever.
Function Argument Types and Result Types
For each function with a fixed #$arity, one must enter into the MELD KB assertions that specify the type of each argument. One does this by using the predicates #$arg1Isa, #$arg2Isa, etc., just the same as for predicates.
Functions with no fixed #$arity still can have their arguments typed with #$argsIsa, which specifies a single type of which every argument must be an instance. Additionally, #$arg1Isa, #$arg2Isa, etc. can be used to further constrain particular arguments. Any argument which isn't explicitly constrained by an #$arg3Isa, e.g., will be constrained by the #$argsIsa constraint. I.e., one makes one assertion to this effect, for a MELD function, by using the predicate #$argsIsa, which specifies a single type of which every argument (besides the ones which are typed by #$arg1Isa, #$arg2Isa,. . . ) must be an instance. Often, all one needs is the #$argsIsa assertion. E.g., the addition function takes any number of arguments, and they'd better all be numbers, so we assert (#$argsIsa #$PlusFn #$Number ).
Functions differ from predicates in that they return a MELD term as a result. In other words, instead of just thinking of them evaluating to a truth value (#$True or #$False), think of them evaluating to some other sort of value, such as a number, a country,. . . -- whatever the type of the result happens to be.
Accordingly, function definitions must also describe the type of the result to be returned by that function; this is done using the predicate #$resultIsa. E.g., (#$resultIsa #$PlusFn #$Number ), since the result of adding up any number or numbers is itself going to be a number.
To put all this together, consider, for example, the function #$GovernmentFn:
(#$arity #$GovernmentFn 1) (#$arg1Isa #$GovernmentFn #$GeopoliticalEntity ) (#$resultIsa #$GovernmentFn #$RegionalGovernment )
This function takes exactly one argument. The argument to #$GovernmentFn must always be an instance of #$GeopoliticalEntity, such as #$Canada. A NAT created using #$GovernmentFn will always be an instance of #$RegionalGovernment. The entire NAT can be used practically anywhere that a regional government atomic term (like #$Canada) could have been used. So, for instance,
(#$isa (#$GovernmentFn #$UnitedStatesOfAmerica) #$RegionalGovernment )
is both syntactically well formed and also happens to be provably #$True, given the #$resultIsa of #$GovernmentFn.
Not only does the NAT approach cut down on the explosion of vocabulary terms, it sometimes makes assertions much more terse and natural-sounding. For example, to assert the rule that "the head of state of a geopolitical entity typically resides in the capital of that geopolitical entity", we could just say:
(#$forAll ?x (#$residesIn ( #$HeadOfStateFn ?x ) ( #$CapitalFn ?x ) ) )
Individual Denoting Functions vs.Collection Denoting Functions
Most functions are instances of either #$IndividualDenotingFunction or #$CollectionDenotingFunction. #$GovernmentFn is an example of the former, since a NAT like ( #$GovernmentFn #$UnitedStatesOfAmerica ) denotes an individual government. On the other hand, #$FruitFn is an example of the latter, since a NAT like (#$FruitFn #$AppleTree) denotes the collection of all apples, not an individual apple.
The definition of each instance of #$CollectionDenotingFunction should specify not only its argument types and result type, but also the collection(s) which the result will have as supersets (in many cases, "supersets" is expressed using the predicate #$genls.) This constraining is done using the predicate #$resultGenl. For example, consider the function #$LeftPairMemberFn. When applied to the argument #$Shoe (the set of all shoes), it should return as its value the set of all left shoes. The MELD function #$LeftPairMemberFn has the following formulas involving its asserted to be true in both the Cyc KB and in the HPKB IKB -- among other formulas involving #$LeftPairMemberFn which are also true in those MELD KBs -- thereby partially defining it; note in particular the last (fifth) of these assertions:
(#$isa #$LeftPairMemberFn #$CollectionDenotingFunction )
(#$arity #$LeftPairMemberFn 1 )
(#$arg1Isa #$LeftPairMemberFn #$SymmetricalPartType )
(#$resultIsa #$LeftPairMemberFn #$ExistingObjectType )
(#$resultGenl #$LeftPairMemberFn #$LeftObject )
Then the following must be true concerning the NAT (#$LeftPairMemberFn #$Shoe), a NAT constructed from #$LeftPairMemberFn and #$Shoe:
(#$isa (#$LeftPairMemberFn #$Shoe ) #$ExistingObjectType )
(#$genls (#$LeftPairMemberFn #$Shoe) #$LeftObject)
In other words, the set of left shoes is an instance of the collection #$ExistingObjectType and a subset of the collection #$LeftObject. Each instance of (#$LeftPairMemberFn #$Shoe) will thereby have inferred about it such facts as: its being an existing partially-tangible object, a left-object, an opaque object, etc.
To have it also inferred to be a shoe, we would have to add another axiom; there are many possible ones that would do the job; a good one to assert would be this terse general formula:
(#$forAll ?x ( #$genls ( #$LeftPairMemberFn ?x ) ?x ) )
Microtheories
A #$microtheory, or context, is a bundle (set) of formulas in the KB. Each formula must be asserted in at least one microtheory. Thus a particular formula might be contained in many microtheories, but each particular assertion of that formula was just made into one single microtheory at the time that assertion was made.
Microtheories are fully reified objects, and thus they can not only contain MELD formulas, they can also participate in MELD formulas. Some predicates that take microtheories as arguments might include those with names such as #$ist, #$assumptions , #$genlMts, #$finerGranularityMt, #$temporallyEarlierMt,, etc.
#$ist
The #$ist predicate lets one state, or find out, the "content" assertions of a #$microtheory;
(#$ist MICRO1 PROP1)
means that the proposition PROP1 is asserted to be contained in ("true in") microtheory MICRO1.
#$assumptions
The #$assumptions predicate lets one find out the partial definition of what this context is all about: the things that may be assumed to be true in this context that set it apart from other contexts in the knowledge base. Any explicit assumptions of a microtheory become extra conjuncts in the antecedent (left-hand-side) of any implication taken ("lifted") from the microtheory to another context.
For example, many microtheories are about ordinary circumstances on the Earth; they have as #$assumptions propositions that solid objects have weight, that walking occurs on a ground or floor, etc. These assumptions apply to every assertion and rule in the microtheory, and it would be a nuisance to have to put them in the antecedent of every rule.
But, when the rule is moved to a new microtheory, say one covering both the Earth and outer space, the rules will then have those assumptions as explicit conditions.
#$genlMt
The #$genlMt predicate interrelates two microtheories, so that
(#$genlsMt MICRO1 MICRO2)
means that the first microtheory MICRO1 has access to all the assertions in the second, MICRO2.
Thus, if (#$ist MICRO2 PROP1) and (#$genlsMt MICRO1 MICRO2), then you can infer (#$ist MICRO1 PROP1).
This is one way in which a formula is effectively lifted from one #$microtheory into another. The #$genlsMt link induces a partial ordering (a transitive subsumption hierarchy) on the set of all microtheories.
Cross Microtheory Logic
In general, logic does not carry over across microtheories. If P is true in Mt1, and P => Q is true in Mt2, then one cannot in general conclude Q to be true anywhere. If one has, or creates, a microtheory which is the union of Mt1 and Mt2, as it were, then Q would be true in that microtheory.
A special case of this would occur if one of the two microtheories were known (e.g., via #$genlMt) to be a specialization of the other; then Q would be true in that more specialized context.
Formally, every formula asserted to the KB, whether originally asserted or deduced, must be asserted in some microtheory that is in the KB. A system communicating in MELD that does not have a built-in system of microtheories like this can simply have all its assertions, rules and queries deemed to be in one big (outermost, virtual) microtheory.
A well-formed assertion complies with MELD if it either is asserted without a microtheory designation (in which case it goes into the outermost, default microtheory of the KB), or if it is asserted within an explicit ist statement or by some other means of directing it to a particular microtheory.
The most practical reason for having the microtheory mechanism is as a heuristic for knowledge-entering (KEing) and a heuristic for performing inference. As regards KEing, it helps make assertions terser, and in cases where only some of the assumptions have been made explicit it keeps the knowledge enterer from accidentally making contradictory statements to the KB.
As regards inferencing, it helps guide inference, first because the intra-microtheory assertions are the only ones to examine first as they are the only ones guaranteed a priori to be true together with each other, and second through the various inter-microtheory predicates (such as #$genlMt, #$finerGranularityMt, #$temporallyEarlierMt, ... ) as a way of guiding the search to gradually less relevant portions of the KB, rather than having to treat all the entries in the KB as potentially equally likely to be relevant.
This complements and augments any other relevance heuristics which one might assert declaratively into the KB, or build in via the introduction of procedural Heuristic Level inference modules.
Truth Values
Each formula has an associated truth value (in each microtheory). One could define predicates such as monotonicallyTrue, and make these assertions declaratively about each and every assertion in the KB. Pragmatically, most MELD interfaces and implementations support some more economical way of doing that tagging. MELD contains five possible non-numeric truth values, of which the most common are default true and monotonically true. The other truth values are default false, monotonically false, and unknown. In addition, MELD accommodates Bayesian probabilities and dependencies, and (separately) fuzzy truth values, attributes and sets, as described below. All MELD-compliant system must support at least one "true" and one "false".
Monotonically true
- Monotonically true means: true with no exceptions. Assertions which are monotonically true are held to be true in every case, that is, for every possible set of bindings -- not just currently-known-about bindings -- to the universally quantified variables (if any) in the assertion, and cannot be overridden.
In the case of a monotonically true assertion with universally quantified variables in its formula, if an object is found for which the assertion is not true:
- some sort of MELD warning message should be signaled, and
- presumably the user interface that is implemented will do something with this error, such as
- report it to the user,
- ask which of the offending assertions to remove or change,
- ask for some new assumption which would keep the contradiction from occurring, etc.
In the case of a ground assertion that is monotonically true, if the negation of that formula is ever asserted or arrived at during inference (in the same microtheory), the system may elect to:
- reject the assertion flat out (i.e., the earlier ones win over the new contradictory one), or
- it may do the opposite (allowing new information to override old).
In either case, a genuine MELD error should be signaled to the user (via the interface) giving notice of the logical contradiction. This digression into implementation and interface concerns is more properly the subject of Appendix B, below, so we will not pursue it further here.
Default True
- Assertions which are default true, in contrast to monotonically true, can have exceptions. They are held to be true only in most cases (usually meaning most of the relevant cases likely to encountered in the current context), and can be overridden without the need for alerting the user, though some interface tools may want to gently keep the user abreast of such overridings. Even if, in the same #$microtheory, negation of an existing ground, default assertion is asserted or is arrived at through inference, no error results or is signaled. Instead, the system's argumentation mechanism is invoked to decide what the final truth value of the assertion will be.
Monotonic True vs Default True
A monotonic truth value always "beats" a default truth value of the same assertion. If something is known to be monotonically true, but is also known to be default false, it is monotonically true. This is determined by the multi-valued truth tables for the logical connectives.
MELD argumentation system
The argumentation system (used in both the Cyc inference system and the HPKB MELD inference system) says that if there is at least one positive argument, and each negative one has some positive one that is more preferred, then go ahead and believe the assertion to be true. Thus there can be axioms whose consequents conclude "preferred" (of one argument over another) and which check arguments for validity. Arguments are like proofs, but they can contain assumptions and can depend on conclusions which themselves were only arrived at through inference and at the default-true level of truth.
exceptions & overriding default true
Several declarative mechanisms exist in the Cyc KB and the IKB (and therefore have MELD support in their respective MELD implementations), for manual overriding of default true assertions.
These include the predicate "#$overrides", to indicate a preference for one assertion over another, the predicate "#$exceptFor", to cite individuals who are exceptions to rules, and the predicate "#$exceptWhen", to indicate situations which are exceptions to rules.
For example:
(#$exceptWhen (#$isa ?BIRD #$Penguin) (#$implies (#$isa ?BIRD #$Bird ) (#$skillCapableOf ?BIRD #$Flying-FlappingWings #$performedBy ) ) )
states that penguins are an exception to the rule that all birds can fly.
GAFs vs Rules
By default, GAFs (formulae containing no variables) which begin with the predicates #$isa and #$genls are monotonically true, while all other assertions (including rules) are default true.
Alternate logic reasoning systems
No system using the MELD language is required to support any nonmonotonic logic, probabilistic reasoning system, or system of fuzzy, partial or multiple truth values, so long as it has at least one "true" and one "false" that are transformed by negation. However, systems with any of these features should support the relevant MELD syntactic forms associated with that feature.
Probabilities, including Bayesian (Pearlian) nets
Any assertion can have 'a priori' (an a priori, possibly "subjective") probability associated with it in a particular context. MELD makes no assumption as to the original basis or reason for assigning the probability.
The value is the probability assigned to an assertion in a range from zero to one. Zero means certainly #$false and one means certainly #$true, according to that #$microtheory.
Stating Prior and Derived Probabilities
The expression of the a priori probability of an assertion (in a particular microtheory) can be thought of in the following way:
(#$priorProbability #$Assertion1 .8 )
where, given (only) the domain assumptions (indicated with the #$domainAssumptions relation) of the #$microtheory, the probability of Assertion1 is 0.8.
For the probability when more is known, including assertions and conclusions in the microtheory, use:
(#$derivedProbability #$Assertion1 .8 )
The predicate #$derivedProbability states that the probability of Assertion1 is 0.8 based on its prior probability and on all other assertions that we that we know to be true and relevant in this context, where those other assertions affect Assertion1.
The relevant assertions affecting the likelihood of Assertion1 may be partially ordered in a Bayesian Network N, which has been set up and linked to that microtheory by the predicate #$bayesNetOfMicrotheory.
Calculating Prior and Derived Probabilities
Or, the derived likelihood may be calculated using some other probabilistic theory. (It is assumed that only one probabilistic system, or a compatible set of them, will be in use in one microtheory at one time.)
Two functions based on these predicates are:
(#$PriorProbabilityFn A)
which returns the prior probability of assertion A in the current context, and
(#$DerivedProbabilityFn A)
which returns the probability of assertion A derived from its prior probability and the other, relevant assertions in the context (e.g. using a Bayesian net).
Weak Constraints
The foregoing constants assume nothing about frequentism, the sample space, distributions, etc.; they only conform to the very weak constraint described below.
Second-Order and Higher-Order probabilities
The predicates #$priorProbability and #$derivedProbability can be nested to provide second-order and higher-order probabilities.
In addition, there are variants of these predicates and functions that allow for a range of probability, such as "80 to 90 percent likely" or "the odds are over twenty to one".
These are: #$priorProbabilityRange, #$PriorProbabilityRangeFn, #$derivedProbabilityRange, and #$DerivedProbabilityRangeFn.
Relative Probability
For non-numeric assertions of relative probability, MELD has
(#$lessLikelyThan-Prior A B)
which, with no commitment as to the absolute probabilities of assertions A or of B, states that A has higher prior probability than B has (considering only the explicit domain assumptions of the Microtheory).
MELD also has (#$lessLikelyThan-Derived A B) in which A is more likely than B given not only the domain assumptions of the microtheory, but also all the assertions asserted in the #$microtheory.
Single Dependency Conditional Probability
MELD also has a representation for conditional dependence probability. The predicate (#$conditionalProbability A B PROB) is a relation of two assertions and a probability --- the conditional probability of A being true given that B is known to be true, along with the domain assumptions, regardless of any other known facts.
Similarly the function (#$ConditionalProbabilityFn A B) is a function of two assertions; it returns the conditional probability of A being true given that B is known to be true, along with the domain assumptions, regardless of any other known facts.
Multiple Dependency Conditional Probability
The conditional probability can be conditioned on a set of assertions rather than a single one.
Use
(#$conditionalProbabilitySet A SET PROB)
to assert that the likelihood of A, given the truth of all the assertions in SET and the domain assumptions, regardless of any other facts, is PROB.
The function version of this is
(#$ConditionalProbabilitySetFn A SET)
given the A and the set of assertions while returning the PROBNO.
Related to these is the predicate (#$conditionallyIndependent A B) which says that there is no direct conditional dependence in either direction between assertions A and B, irrespective of other knowledge,
i.e. that
(#$equals (#$PriorProbabilityFn (#$and ?A ?B ) ) (#$TimesFn (#$PriorProbabilityFn ?A) (#$PriorProbabilityFn ?B) ) )
A related predicate,
(#$conditionallyIndependent-Given A B C)
is a predicate that states that assertions A and B are conditionally mutually independent given knowledge of the truth of assertion C (and any domain assumptions of the microtheory) irrespective of any other knowledge.
Note that this does not require knowledge of the actual truth of C, just whether such knowledge would be relevant to the mutual independence of A and B.
If you wish to base the independence of A and B on the truth of a whole set of assertions, instead of just a single assertion C, use the variant:
(#$conditionallyIndependent-GivenSet A B SET).
Bayes Nets
For Pearl's theory of Bayesian Networks, an instance of the collection #$BayesNet is created for a particular #$microtheory.
Each #$BayesNet is a directed acyclic graph in which the nodes are random variables for assertions and the links are instances of the predicate #$bayesParent.
The instance of #$BayesNet is explicitly associated with the microtheory by using the predicate
(#$bayesNetOfMicrotheory NET MT).
The predicate (#$bayesParent A B NET) means that the assertion B has been identified as a Bayesian immediate predecessor or probabilistic "cause" of assertion A, i.e. that A and B are directly linked as (possibly mutually) dependent in the Bayesian sense, in an acyclic graph NET or "Bayesian Network" of assertions, and that Pearl's principle of directedness assigns a "causal" direction from B to A in NET. A may have any finite number of Pearlian/Bayesian predecessors or "causes" in NET.
(Note that the constant-name "#$bayesParent" may be changed to "#$bayesParents" in the near future under Cyc's predicate-naming convention, reflecting the fact that a node may have multiple parents.]
An alternative notation for the same thing, but with a set of parent-nodes, is
(#$bayesParentSet A SET NET)
where A is an assertion and SET is the set of all Pearlian/Bayesian predecessors of A in the #$BayesNet NET.
Similarly, the function (#$BayesParentSetFn A NET) returns the set of all Pearlian/Bayesian predecessors of assertion A in #$BayesNet NET.
In both of the latter cases, the set of predecessors may be the empty set when the assertion A corresponds to a source-node in the net NET. It is common to create such networks without knowing in advance any prior probabilities of any assertions in the network.
Note that the network NET itself is always a reified object subject to further description, an instance of the collection #$BayesNet.
Constraints on Probability Systems
Any system of probabilities as described above must obey the following weak constraint within any one microtheory: No assertion can have probability zero and be monotonically true, and no assertion can have probability one and be monotonically false. MELD imposes no further constraints than this; individual implementations may relate probabilities to the five truth values in various more elaborate ways, if this constraint is adhered to.
Fuzzy Sets & Truth Values
Every assertion can have a fuzzy value associated with it. The fuzzy value of an assertion is represented in the following way:
(#$fuzzyTruthValue #$Assertion1 .2)
where .2 is the fuzzy value assigned to #$Assertion1. The value can range from zero to one, or over any sub-interval. A fuzzy value does not represent probability; rather, it refers to degree of truth, which may be certainly known regardless of its fuzzy value.
An assertion could be
- certainly fuzzily true,
- uncertainly fuzzily true,
- uncertainly crisply true, etc.
MELD represents fuzzy sets with the collection #$FuzzySetOrCollection, each instance of which is a set or collection with a fuzzy membership function.
For any thing ?X, if ?FSC is an instance of #$FuzzySetOrCollection then
(#$FuzzyMembershipFn FSC )
yields a #$FuzzyTruthValue between zero and one. There is also a predicate form of this:
(#$fuzzyMembership FSC VAL ), meaning that the fuzzy truth of the membership of X in FSC is VAL.
MELD represents fuzzy attribute values similarly with instances of the collection #$FuzzyAttributeValue and #$FuzzyAttributeType.
MELD is not committed to any particular system of interpreting connectives with fuzzy values except that zero should correspond to falsehood or nonmembership. MELD does not assume the MAX/MIN treatment of "and" and "or", but allows any system of norms and conorms that handle the zero case as falsehood.
Supports
Associated with each formula in the MELD KB (and, at an implementation level, most likely part of each assertion data structure) is a support, which consists of one or more justifications which form the support for that formula in that KB. In many cases, at least one of the supporting justifications is local, indicating that the assertion was added to the KB from an outside source. In other cases, a supporting justification is a source which indicates the assertion was inferred and which outlines the final step of some argument, or chain of reasoning, which supports the assertion. Supports for assertions in the KB can be thought of as follows:
(#$support Assertion1 Support1)
where Support1 is a chain of arguments supporting Assertion1. Note that there may be more than one support for a given assertion. In this case, there will be more than one support meta-assertion for that assertion. The support predicate is a way to get at the arguments for a formula.
Appendix A: Formulas true in every MELD KB
As we remarked above, the syntactic component of MELD includes a large number of constant terms (you can think of these as "reserved words" in the MELD language), and the semantic component of MELD includes a large number of sentences involving and interrelating these terms. This set of sentences forms a coherent self-sufficient KB -- the MELD KERNEL KB -- which forms the upper (most general) part of every MELD KB, including, e.g., the Cyc KB, the HPKB IKB, etc.
Herewith is that list of approximately 650 sentences -- each is a closed, well-formed MELD formula.
All of the MELD constants mentioned in these assertions should be thought of as MELD "reserved words." These terms, of which there are about 160, occur below on comment lines, just before the set of mandatory formulas involving them; each of those comment lines begins with three semicolons in a row; e.g., ;;; #$AntiSymmetricBinaryPredicate.
The formulas, and terms, are not commented or explained, below. If one browses through the Cyc KB or the HPKB IKB, one can read the documentation for each of these terms, etc. That is how you, a human reader, can most easily become familiar with the ontology and the semantics of MELD. Just as the BNF in Appendix C, the long list of formulas below (here in Appendix B) is provided more to be machine- than human- readable.
We've arranged these in such a fashion that (most) duplicates have been eliminated. Thus, in the case of one of the first few assertions,
(#$genls #$AntiSymmetricBinaryPredicate #$BinaryPredicate),
that assertion is listed once, under ;;; #$AntiSymmetricBinaryPredicate, not again under ;;; #$BinaryPredicate.
We've prefixed each MELD term with the characters #$. This may facilitate reading mechanically; if you don't care or want this, just do a systematic replace of #$ by the empty string. It will be useful in distinguishing MELD constant names from the names of C (or Lisp) functions which are called to implement some of the low-level bookkeeping, and may be useful in distinguishing MELD constant names from numbers (e.g., distinguishing the MELD constant named 42 from the number 42.)
Let us reiterate that MELD is a declarative language with no procedural information of any kind in any MELD formula, including these formulas.
Finally, you may notice that about 10 of the 160 MELD constant terms below contain the word "Cyc"; this reflects the origins of those terms. We could just as well have called those ten . . .Cyc. . . terms . . .MELD. . . instead; the absolute names are not so important as agreeing on a fixed vocabulary of names for constants.
This is the MELD semantic standard; please do not rename any of these 160 terms, or remove/violate any of these 650 formulas:
;;; #$AntiSymmetricBinaryPredicate
001 (#$isa #$AntiSymmetricBinaryPredicate #$Collection )
002 (#$genls #$AntiSymmetricBinaryPredicate #$BinaryPredicate )
003 (#$implies (#$and (#$isa ?SLOT #$AntiSymmetricBinaryPredicate) (#$isa ?SLOT #$IrreflexiveBinaryPredicate) ) (#$isa ?SLOT #$AsymmetricBinaryPredicate) )
;;; #$Assertion
004 (#$isa #$Assertion #$Collection)
005 (#$genls #$Assertion #$CycIndexedTerm)
006 (#$genls #$Assertion #$IndividualObject)
;;; #$AsymmetricBinaryPredicate
007 (#$isa #$AsymmetricBinaryPredicate #$Collection )
008 (#$genls #$AsymmetricBinaryPredicate #$AntiSymmetricBinaryPredicate )
009 (#$genls #$AsymmetricBinaryPredicate]] #$IrreflexiveBinaryPredicate )
010 (#$not (#$and (#$isa ?PRED #$AsymmetricBinaryPredicate) (?PRED ?ARG1 ?ARG2) (?PRED ?ARG2 ?ARG1) ) )
011 (#$implies (#$and (#$isa ?Q #$AsymmetricBinaryPredicate) (#$genlPreds ?P ?Q) ) (#$isa ?P #$AsymmetricBinaryPredicate) )
012 (#$implies (#$isa ?PRED #$AsymmetricBinaryPredicate) (#$negationInverse ?PRED ?PRED) )
;;; #$AttributeValue
013 (#$isa #$AttributeValue #$Collection)
014 (#$genls #$AttributeValue #$IndividualObject)
;;; #$BaseKB
015 (#$isa #$BaseKB #$BroadMicrotheory)
016 (#$implies (#$isa ?MIC #$Microtheory) (#$genlMt ?MIC #$BaseKB) )
;;; #$BinaryPredicate
017 (#$isa #$BinaryPredicate #$Collection)
018 (#$genls #$BinaryPredicate #$Predicate)
019 (#$implies (#$isa ?P #$BinaryPredicate) (#$arity ?P 2 ) )
;;; #$BookkeepingMt
020 (#$isa #$BookkeepingMt #$Microtheory)
021 (#$genlMt #$BookkeepingMt #$CyclistsMt)
022 (#$genlMt #$BookkeepingMt #$BaseKB)
;;; #$BookkeepingPredicate
023 (#$isa #$BookkeepingPredicate #$Collection)
024 (#$genls #$BookkeepingPredicate #$Predicate)
;;; #$BroadMicrotheory
025 (#$isa #$BroadMicrotheory #$Collection)
026 (#$genls #$BroadMicrotheory #$Microtheory)
;;; #$Collection
see also 023. 025
027 (#$isa #$Collection #$Collection)
028 (#$genls #$Collection #$SetOrCollection)
;;; #$CollectionDenotingFunction
029 (#$isa #$CollectionDenotingFunction #$Collection)
030 (#$genls #$CollectionDenotingFunction #$ReifiableFunction )
;;; #$CommutativeRelation
031 (#$isa #$CommutativeRelation #$Collection)
032 (#$genls #$CommutativeRelation #$Relationship)
;;; #$CycELVariable
033 (#$isa #$CycELVariable #$Collection)
034 (#$genls #$CycELVariable #$CycSystemSymbol)
;;; #$CycExpression
035 (#$isa #$CycExpression #$Collection )
036 (#$genls #$CycExpression #$IndividualObject)
;;; #$CycFormula
037 (#$isa #$CycFormula #$Collection)
038 (#$genls #$CycFormula #$CycExpression)
;;; #$CycIndexedTerm
039 (#$isa #$CycIndexedTerm #$Collection)
040 (#$genls #$CycIndexedTerm]] #$Thing)
;;; #$CycSystemList
041 (#$isa #$CycSystemList #$Collection)
042 (#$genls #$CycSystemList #$IndividualObject)
;;; #$CycSystemString
043 (#$isa #$CycSystemString #$Collection)
044 (#$genls #$CycSystemString #$IndividualObject)
;;; #$CycSystemSymbol
045 (#$isa #$CycSystemSymbol #$Collection)
046 (#$genls #$CycSystemSymbol #$IndividualObject )
;;; #$Cyclist
047 (#$isa #$Cyclist #$Collection )
048 (#$genls #$Cyclist #$TemporalObject )
;;; #$CyclistsMt
049 (#$isa #$CyclistsMt #$Microtheory )
050 (#$genlMt #$CyclistsMt #$BaseKB)
;;; #$DefaultMonotonicPredicate
051 (#$isa #$DefaultMonotonicPredicate #$Collection)
052 (#$genls #$DefaultMonotonicPredicate #$Predicate)
;;; #$EvaluatableFunction
053 (#$isa #$EvaluatableFunction #$Collection)
054 (#$genls #$EvaluatableFunction #$FunctionTheMathematicalType )
;;; #$False
055 (#$isa #$False #$IndividualObject )
;;; #$Format
056 (#$isa #$Format #$Collection )
057 (#$genls #$Format #$IndividualObject )
;;; #$ForwardInferencePSC
058 (#$isa #$ForwardInferencePSC #$ProblemSolvingCntxt )
059 (#$genlMt #$ForwardInferencePSC #$BaseKB)
;;; #$FunctionTheMathematicalType
060 (#$isa #$FunctionTheMathematicalType #$Collection)
061 (#$genls #$FunctionTheMathematicalType #$Relationship)
;;; #$Guest
062 (#$isa #$Guest #$HumanCyclist )
;;; #$HumanCyclist
063 (#$isa #$HumanCyclist #$Collection )
064 (#$genls #$HumanCyclist #$Cyclist )
;;; #$IndividualObject
065 (#$isa #$IndividualObject #$Collection )
066 (#$genls #$IndividualObject #$Thing )
;;; #$InferenceRelatedBookkeepingPredicate
067 (#$isa #$InferenceRelatedBookkeepingPredicate #$Collection )
068 (#$genls #$InferenceRelatedBookkeepingPredicate #$BookkeepingPredicate )
;;; #$Integer
069 (#$isa #$Integer #$Collection )
070 ( #$genls #$Integer #$RealNumber )
;;; #$IntervalEntry
071 ( #$isa #$IntervalEntry #$Format)
;;; #$IrreflexiveBinaryPredicate
072 ( #$isa #$IrreflexiveBinaryPredicate #$Collection )
073 ( #$genls #$IrreflexiveBinaryPredicate #$BinaryPredicate )
074 (#$not (#$and (#$isa ?PRED #$IrreflexiveBinaryPredicate) (?PRED ?OBJ ?OBJ) ) )
075 (#$implies (#$and (#$isa ?Q #$IrreflexiveBinaryPredicate) (#$different ?P ?Q) (#$genlPreds ?P ?Q) ) (#$isa ?P #$IrreflexiveBinaryPredicate) )
;;; #$ListTheFormat
076 (#$isa #$ListTheFormat #$Format)
;;; #$Microtheory
077 (#$isa #$Microtheory #$Collection )
078 (#$genls #$Microtheory #$IndividualObject)
;;; #$NonNegativeInteger
079 (#$isa #$NonNegativeInteger #$Collection)
080 (#$genls #$NonNegativeInteger #$Integer)
;;; #$NonPredicateFunction
081 (#$isa #$NonPredicateFunction #$Collection )
082 (#$genls #$NonPredicateFunction #$FunctionTheMathematicalType )
;;; #$PositiveInteger
083 (#$isa #$PositiveInteger #$Collection )
084 (#$genls #$PositiveInteger #$NonNegativeInteger )
;;; #$Predicate
085 (#$isa #$Predicate #$Collection)
086 (#$genls #$Predicate #$FunctionTheMathematicalType )
;;; #$ProblemSolvingCntxt
087 (#$isa #$ProblemSolvingCntxt #$Collection )
088 (#$genls #$ProblemSolvingCntxt #$Microtheory )
;;; #$QuaternaryPredicate
089 (#$isa #$QuaternaryPredicate #$Collection)
090 (#$genls #$QuaternaryPredicate #$Predicate )
091 (#$implies (#$isa ?P #$QuaternaryPredicate ) (#$arity ?P 4 ) )
;;; #$QuintaryPredicate
092 (#$isa #$QuintaryPredicate #$Collection)
093 (#$genls #$QuintaryPredicate #$Predicate)
094 (#$implies (#$isa ?P #$QuintaryPredicate ) (#$arity ?P 5) )
;;; #$RealNumber
095 (#$isa #$RealNumber #$Collection )
096 (#$genls #$RealNumber #$AttributeValue )
;;; #$ReflexiveBinaryPredicate
097 (#$isa #$ReflexiveBinaryPredicate #$Collection )
098 (#$genls #$ReflexiveBinaryPredicate #$BinaryPredicate )
099 (#$implies (#$isa ?PRED #$ReflexiveBinaryPredicate ) (?PRED ?OBJ ?OBJ) )
;;; #$ReifiableFunction
100 (#$isa #$ReifiableFunction #$Collection )
101 (#$genls #$ReifiableFunction #$NonPredicateFunction )
;;; #$ReifiableTerm
102 (#$isa #$ReifiableTerm #$ReifiableTerm )
103 (#$isa #$ReifiableTerm #$Collection )
104 (#$genls #$ReifiableTerm #$CycIndexedTerm )
;;; #$Relationship
105 (#$isa #$Relationship #$Collection)
106 (#$genls #$Relationship #$IndividualObject )
;;; #$Set-Mathematical
107 (#$isa #$Set-Mathematical #$Collection)
108 (#$genls #$Set-Mathematical #$SetOrCollection)
;;; #$SetOrCollection
109 (#$isa #$SetOrCollection #$Collection )
110 (#$genls #$SetOrCollection #$Thing )
;;; #$SetTheFormat
111 (#$isa #$SetTheFormat #$Format)
;;; #$SiblingDisjointAttributeType
112 (#$isa #$SiblingDisjointAttributeType #$SiblingDisjointCollection)
113 (#$genls #$SiblingDisjointAttributeType #$Collection)
114 (#$implies (#$and (#$isa ?C #$SiblingDisjointAttributeType ) (#$isa ?A1 ?C ) (#$isa ?A2 ?C ) (#$different ?A1 ?A2 ) (#$hasAttributes ?G072 ?A1 ) (#$hasAttributes ?G072 ?A2 ) ) (#$or (#$genlAttributes ?A1 ?A2) (#$genlAttributes ?A2 ?A1) ) )
;;; #$SiblingDisjointCollection
115 (#$isa #$SiblingDisjointCollection #$Collection)
116 (#$genls #$SiblingDisjointCollection #$Collection)
;;; #$SingleEntry
117 (#$isa #$SingleEntry #$Format )
;;; #$SkolemFuncN
118 (#$isa #$SkolemFuncN #$ReifiableFunction)
119 (#$arity #$SkolemFuncN 3)
120 (#$arg1Isa #$SkolemFuncN #$CycSystemList)
121 (#$arg2Isa #$SkolemFuncN #$CycSystemSymbol )
122 (#$arg3Isa #$SkolemFuncN #$RealNumber)
;;; #$SkolemFunction
123 (#$isa #$SkolemFunction #$Collection)
124 (#$genls #$SkolemFunction #$ReifiableFunction)
125 (#$arity #$SkolemFunction 2 )
126 (#$arg2Isa #$SkolemFunction #$CycSystemSymbol)
127 (#$arg1Isa #$SkolemFunction #$CycSystemList)
;;; #$SubAbs
128 (#$isa #$SubAbs #$Format)
;;; #$SymmetricBinaryPredicate
129 (#$isa #$SymmetricBinaryPredicate #$Collection)
130 (#$genls #$SymmetricBinaryPredicate #$CommutativeRelation )
131 (#$genls #$SymmetricBinaryPredicate #$BinaryPredicate )
132 (#$implies (#$and (#$isa ?PRED #$SymmetricBinaryPredicate) (?PRED ?ARG1 ?ARG2) ) (?PRED ?ARG2 ?ARG1) )
133 (#$implies (#$isa ?PRED #$SymmetricBinaryPredicate ) (#$genlInverse ?PRED ?PRED ) )
;;; #$TemporalObject
134 (#$isa #$TemporalObject #$Collection)
135 (#$genls #$TemporalObject #$IndividualObject )
;;; #$TernaryPredicate
136 (#$isa #$TernaryPredicate #$Collection )
137 (#$genls #$TernaryPredicate #$Predicate )
138 (#$not (#$and (#$isa ?X #$TernaryPredicate ) (#$arg4Isa ?X ?Y ) ) )
139 (#$implies (#$isa ?P #$TernaryPredicate ) (#$arity ?P 3 ) )
;;; #$TheSet
140 (#$isa #$TheSet #$VariableArityRelation ) 141 (#$isa #$TheSet #$NonPredicateFunction) 142 (#$resultIsa #$TheSet #$Set-Mathematical) 143 (#$argsIsa #$TheSet #$Thing )
;;; #$TheTerm
144 (#$isa #$TheTerm #$Collection )
145 (#$genls #$TheTerm #$Thing )
;;; #$Thing
146 (#$isa #$Thing #$Collection )
147 (#$isa ?OBJ #$Thing)
;;; #$TransitiveBinaryPredicate
148 (#$isa #$TransitiveBinaryPredicate #$Collection )
149 (#$genls #$TransitiveBinaryPredicate #$BinaryPredicate)
150 (#$implies (#$and (#$isa ?U #$TransitiveBinaryPredicate ) ( ?U ?X ?Z ) ( ?U ?Z ?VAR3 ) ) ( ?U ?X ?VAR3 ) )
;;; #$True
151 (#$isa #$True #$IndividualObject )
;;; #$UnaryPredicate
152 (#$isa #$UnaryPredicate #$Collection )
153 (#$genls #$UnaryPredicate #$Predicate )
154 (#$implies (#$isa ?P #$UnaryPredicate ) (#$arity ?P 1 ) )
;;; #$UnaryTypePredicate
155 (#$isa #$UnaryTypePredicate #$Collection )
156 (#$genls #$UnaryTypePredicate #$UnaryPredicate )
157 (#$genls #$UnaryTypePredicate #$InferenceRelatedBookkeepingPredicate )
;;; #$VariableArityRelation
158 (#$isa #$VariableArityRelation #$Collection )
159 (#$genls #$VariableArityRelation #$Relationship )
;;; #$abnormal
160 (#$isa #$abnormal #$DefaultMonotonicPredicate )
161 (#$isa #$abnormal #$BinaryPredicate )
162 (#$arity #$abnormal 2 )
163 (#$arg1Isa #$abnormal #$CycSystemList )
164 (#$arg2Isa #$abnormal #$Assertion )
;;; #$afterAdding
165 (#$isa #$afterAdding #$InferenceRelatedBookkeepingPredicate )
166 (#$isa #$afterAdding #$BinaryPredicate )
167 (#$arity #$afterAdding 2 )
168 (#$arg1Isa #$afterAdding #$Predicate )
169 (#$arg2Isa #$afterAdding #$CycSystemSymbol )
;;; #$afterRemoving
170 (#$isa #$afterRemoving #$InferenceRelatedBookkeepingPredicate )
171 (#$isa #$afterRemoving #$BinaryPredicate )
172 (#$arity #$afterRemoving 2 )
173 (#$arg1Isa #$afterRemoving #$Predicate )
174 (#$arg2Isa #$afterRemoving #$CycSystemSymbol)
;;; #$and
175 (#$isa #$and #$CommutativeRelation )
176 (#$isa #$and #$VariableArityRelation )
178 (#$argsIsa #$and #$CycFormula )
179 (#$resultIsa #$and #$CycFormula )
;;; #$arg1Format
180 (#$isa #$arg1Format #$BinaryPredicate)
181 (#$arity #$arg1Format 2 )
182 (#$arg1Isa #$arg1Format #$Predicate )
183 (#$arg2Isa #$arg1Format #$Format )
;;; #$arg1Genl
184 (#$isa #$arg1Genl #$BinaryPredicate )
185 (#$arity #$arg1Genl 2 )
186 (#$arg1Isa #$arg1Genl #$Relationship )
187 (#$arg2Isa #$arg1Genl #$Collection )
;;; #$arg1Isa
188 (#$isa #$arg1Isa #$DefaultMonotonicPredicate )
189 (#$isa #$arg1Isa #$BinaryPredicate )
190 (#$arity #$arg1Isa 2)
191 (#$arg1Isa #$arg1Isa #$Relationship )
192 (#$arg2Isa #$arg1Isa #$Collection )
;;; #$arg2Format
193 (#$isa #$arg2Format #$BinaryPredicate )
194 (#$arity #$arg2Format 2 )
195 (#$arg1Isa #$arg2Format #$Predicate )
196 (#$arg2Isa #$arg2Format #$Format )
;;; #$arg2Genl
197 (#$isa #$arg2Genl #$BinaryPredicate )
198 (#$arity #$arg2Genl 2 )
199 (#$arg1Isa #$arg2Genl #$Relationship )
200 (#$arg2Isa #$arg2Genl #$Collection )
;;; #$arg2Isa
201 (#$isa #$arg2Isa #$DefaultMonotonicPredicate )
202 (#$isa #$arg2Isa #$BinaryPredicate )
203 (#$arity #$arg2Isa 2 )
204 (#$arg1Isa #$arg2Isa #$Relationship )
205 (#$arg2Isa #$arg2Isa #$Collection )
;;; #$arg3Format
206 (#$isa #$arg3Format #$BinaryPredicate)
207 (#$arity #$arg3Format 2 )
208 (#$arg1Isa #$arg3Format #$Predicate )
209 (#$arg2Isa #$arg3Format #$Format )
;;; #$arg3Genl
210 (#$isa #$arg3Genl #$BinaryPredicate)
211 (#$arity #$arg3Genl 2)
212 (#$arg1Isa #$arg3Genl #$Relationship)
213 (#$arg2Isa #$arg3Genl #$Collection)
;;; #$arg3Isa
214 (#$isa #$arg3Isa #$DefaultMonotonicPredicate )
215 (#$isa #$arg3Isa #$BinaryPredicate )
216 (#$arity #$arg3Isa 2 )
217 (#$arg1Isa #$arg3Isa #$Relationship )
218 (#$arg2Isa #$arg3Isa #$Collection )
;;; #$arg4Format
219 (#$isa #$arg4Format #$BinaryPredicate)
220 (#$arity #$arg4Format 2 )
221 (#$arg1Isa #$arg4Format #$Predicate)
222 (#$arg2Isa #$arg4Format #$Format)
;;; #$arg4Genl
223 (#$isa #$arg4Genl #$BinaryPredicate ) 224 (#$arity #$arg4Genl 2)
225 (#$arg1Isa #$arg4Genl #$Relationship)
226 (#$arg2Isa #$arg4Genl #$Collection)
;;; #$arg4Isa
227 (#$isa #$arg4Isa #$DefaultMonotonicPredicate)
228 (#$isa #$arg4Isa #$BinaryPredicate)
229 (#$arity #$arg4Isa 2)
230 (#$arg1Isa #$arg4Isa #$Relationship)
231 (#$arg2Isa #$arg4Isa #$Collection)
;;; #$arg5Format
232 (#$isa #$arg5Format #$BinaryPredicate)
233 (#$arity #$arg5Format 2 )
234 (#$arg1Isa #$arg5Format #$Predicate)
235 (#$arg2Isa #$arg5Format #$Format)
;;; #$arg5Genl
236 (#$isa #$arg5Genl #$BinaryPredicate )
237 (#$arity #$arg5Genl 2 )
238 (#$arg1Isa #$arg5Genl #$Relationship )
239 (#$arg2Isa #$arg5Genl #$Collection )
;;; #$arg5Isa
240 (#$isa #$arg5Isa #$DefaultMonotonicPredicate)
241 (#$isa #$arg5Isa #$BinaryPredicate)
242 (#$arity #$arg5Isa 2)
243 (#$arg1Isa #$arg5Isa #$Relationship)
244 (#$arg2Isa #$arg5Isa #$Collection)
;;; #$argsGenl
245 (#$isa #$argsGenl #$BinaryPredicate)
246 (#$arity #$argsGenl 2 )
247 (#$arg1Isa #$argsGenl #$Relationship)
248 (#$arg2Isa #$argsGenl #$Collection)
;;; #$argsIsa
249 (#$isa #$argsIsa #$BinaryPredicate )
250 (#$arity #$argsIsa 2 )
251 (#$arg1Isa #$argsIsa #$Relationship )
252 (#$arg2Isa #$argsIsa #$Collection )
;;; #$arity
253 (#$isa #$arity #$DefaultMonotonicPredicate )
254 (#$isa #$arity #$BinaryPredicate )
255 (#$arity #$arity 2 )
256 (#$arg1Isa #$arity #$Relationship)
257 (#$arg2Isa #$arity #$Integer )
;;; #$coExtensional
258 (#$isa #$coExtensional #$SymmetricBinaryPredicate )
259 (#$isa #$coExtensional #$ReflexiveBinaryPredicate )
260 (#$isa #$coExtensional #$TransitiveBinaryPredicate)
261 (#$genlInverse #$coExtensional #$coExtensional )
262 (#$arity #$coExtensional 2 )
263 (#$arg1Isa #$coExtensional #$Collection )
264 (#$arg2Isa #$coExtensional #$Collection)
;;; #$comment
265 (#$isa #$comment #$BinaryPredicate )
266 (#$arity #$comment 2 )
267 (#$arg1Isa #$comment #$CycIndexedTerm )
268 (#$arg2Isa #$comment #$CycSystemString )
;;; #$cyclistNotes
269 (#$isa #$cyclistNotes #$BinaryPredicate )
270 (#$arity #$cyclistNotes 2 )
271 (#$arg1Isa #$cyclistNotes #$CycIndexedTerm )
272 (#$arg2Isa #$cyclistNotes #$CycSystemString )
;;; #$defnIff
273 (#$isa #$defnIff #$InferenceRelatedBookkeepingPredicate )
274 (#$isa #$defnIff #$BinaryPredicate )
275 (#$arity #$defnIff 2 )
276 (#$arg1Isa #$defnIff #$Collection )
277 (#$arg2Isa #$defnIff #$CycSystemSymbol )
278 (#$implies (#$defnIff ?X ?Y ) (#$defnSufficient ?X ?Y ) )
;;; #$defnNecessary
279 (#$isa #$defnNecessary #$BinaryPredicate)
280 (#$arity #$defnNecessary 2 )
281 (#$arg1Isa #$defnNecessary #$Collection)
282 (#$arg2Isa #$defnNecessary #$CycSystemSymbol)
;;; #$defnSufficient
283 (#$isa #$defnSufficient #$InferenceRelatedBookkeepingPredicate )
284 (#$isa #$defnSufficient #$BinaryPredicate )
285 (#$arity #$defnSufficient 2 )
286 (#$arg1Isa #$defnSufficient #$Collection )
287 (#$arg2Isa #$defnSufficient #$CycSystemSymbol)
;;; #$different
288 (#$isa #$different #$VariableArityRelation )
289 (#$isa #$different #$EvaluatableFunction )
290 (#$isa #$different #$Predicate )
291 (#$argsIsa #$different #$Thing )
292 (#$not (#$different ?OBJ ?OBJ) )
;;; #$disjointWith
293 (#$isa #$disjointWith #$DefaultMonotonicPredicate )
294 (#$isa #$disjointWith #$SymmetricBinaryPredicate )
295 (#$isa #$disjointWith #$IrreflexiveBinaryPredicate )
296 (#$genlInverse #$disjointWith #$disjointWith )
297 (#$arity #$disjointWith 2 )
298 (#$arg1Isa #$disjointWith #$SetOrCollection )
299 (#$arg2Isa #$disjointWith #$SetOrCollection )
300 (#$not (#$and (#$isa ?OBJ ?COL1) (#$isa ?OBJ ?COL2) (#$disjointWith ?COL1 ?COL2) ) )
301 (#$implies (#$and (#$disjointWith ?COL ?SUPERSET ) (#$genls ?SUBSET ?SUPERSET ) ) (#$disjointWith ?COL ?SUBSET ) )
302 (#$not (#$and (#$disjointWith ?X ?Y) (#$genls ?X ?Y) ) )
;;; #$elementOf
303 (#$isa #$elementOf #$BinaryPredicate)
304 (#$arity #$elementOf 2)
305 (#$arg1Isa #$elementOf #$Thing)
306 (#$arg2Isa #$elementOf #$SetOrCollection)
;;; #$equals
307 (#$isa #$equals #$DefaultMonotonicPredicate )
308 (#$isa #$equals #$SymmetricBinaryPredicate )
309 (#$isa #$equals #$ReflexiveBinaryPredicate )
310 (#$isa #$equals #$TransitiveBinaryPredicate )
311 (#$genlInverse #$equals #$equals )
312 (#$arity #$equals 2 )
313 (#$arg1Isa #$equals #$Thing )
314 (#$arg2Isa #$equals #$Thing )
;;; #$exceptFor
315 (#$isa #$exceptFor #$Relatio1nship)
316 (#$arity #$exceptFor 2)
317 (#$arg2Isa #$exceptFor #$Assertion)
318 (#$arg1Isa #$exceptFor #$ReifiableTerm )
;;; #$exceptWhen
319 (#$isa #$exceptWhen #$Relationship)
320 (#$arity #$exceptWhen 2 )
321 (#$arg2Isa #$exceptWhen #$Assertion)
322 (#$arg1Isa #$exceptWhen #$CycFormula)
;;; #$forAll
323 (#$isa #$forAll #$Relationship )
324 (#$arity #$forAll 2 )
325 (#$arg2Isa #$forAll #$CycFormula )
326 (#$arg1Isa #$forAll #$CycELVariable )
;;; #$genlAttributes
327 (#$isa #$genlAttributes #$ReflexiveBinaryPredicate)
328 (#$isa #$genlAttributes #$TransitiveBinaryPredicate)
329 (#$arity #$genlAttributes 2 )
330 (#$arg1Isa #$genlAttributes #$AttributeValue )
331 (#$arg2Isa #$genlAttributes #$AttributeValue)
;;; #$genlInverse
332 (#$isa #$genlInverse #$BinaryPredicate)
333 (#$arity #$genlInverse 2 )
334 (#$arg1Isa #$genlInverse #$BinaryPredicate )
335 (#$arg2Isa #$genlInverse #$BinaryPredicate )
336 (#$implies (#$and (#$genlInverse ?PRED ?GEN-PRED) (?PRED ?ARG1 ?ARG2) ) (?GEN-PRED ?ARG2 ?ARG1) )
337 (#$implies (#$and (#$genlInverse ?SPEC-PRED ?PRED) (#$genlInverse ?PRED ?GENL-PRED) ) (#$genlPreds ?SPEC-PRED ?GENL-PRED) )
338 (#$implies (#$and (#$genlInverse ?SPEC-PRED ?PRED) (#$genlPreds ?PRED ?GENL-PRED) ) (#$genlInverse ?SPEC-PRED ?GENL-PRED) )
339 (#$implies (#$and (#$negationPreds ?GENL-PRED ?NEG-PRED ) (#$genlInverse ?SPEC-PRED ?GENL-PRED ) ) (#$negationInverse ?NEG-PRED ?SPEC-PRED ) )
340 (#$implies (#$and (#$negationInverse ?GENL-PRED ?NEG-PRED ) (#$genlInverse ?SPEC-PRED ?GENL-PRED ) ) (#$negationPreds ?NEG-PRED ?SPEC-PRED ) )
341 (#$implies (#$and (#$genlPreds ?SPEC-PRED ?PRED ) (#$genlInverse ?PRED ?GENL-PRED ) ) (#$genlInverse ?SPEC-PRED ?GENL-PRED ) )
;;; #$genlMt
342 (#$isa #$genlMt #$DefaultMonotonicPredicate)
343 (#$isa #$genlMt #$AntiSymmetricBinaryPredicate )
344 (#$isa #$genlMt #$ReflexiveBinaryPredicate )
345 (#$isa #$genlMt #$TransitiveBinaryPredicate)
346 (#$arity #$genlMt 2)
347 (#$arg1Isa #$genlMt #$Microtheory )
348 (#$arg2Isa #$genlMt #$Microtheory )
;;; #$genlPreds
349 (#$isa #$genlPreds #$AntiSymmetricBinaryPredicate )
350 (#$isa #$genlPreds #$ReflexiveBinaryPredicate )
351 (#$isa #$genlPreds #$TransitiveBinaryPredicate )
352 (#$arity #$genlPreds 2 )
353 (#$arg1Isa #$genlPreds #$Predicate )
354 (#$arg2Isa #$genlPreds #$Predicate )
355 (#$implies (#$and (?PRED ?ARG1) (#$genlPreds ?PRED ?GENL-PRED ) ) (?GENL-PRED ?ARG1) )
356 (#$implies (#$and (#$negationPreds ?GENL-PRED ?NEG-PRED ) (#$genlPreds ?SPEC-PRED ?GENL-PRED ) ) (#$negationPreds ?NEG-PRED ?SPEC-PRED ) )
357 (#$implies (#$and (#$negationInverse ?GENL-PRED ?NEG-PRED ) (#$genlPreds ?SPEC-PRED ?GENL-PRED ) ) (#$negationInverse ?NEG-PRED ?SPEC-PRED ) )
358 (#$implies (#$and (#$genlPreds ?PRED ?GENL-PRED ) (?PRED ?ARG1 ?ARG2 ?ARG3 ?ARG4 ?ARG5 ) ) (?GENL-PRED ?ARG1 ?ARG2 ?ARG3 ?ARG4 ?ARG5 ) )
359 (#$implies (#$and (#$genlPreds ?PRED ?GENL-PRED) (?PRED ?ARG1 ?ARG2 ?ARG3 ?ARG4) ) (?GENL-PRED ?ARG1 ?ARG2 ?ARG3 ?ARG4) )
360 (#$implies (#$and (#$genlPreds ?PRED ?GENL-PRED) (?PRED ?ARG1 ?ARG2 ?ARG3) ) (?GENL-PRED ?ARG1 ?ARG2 ?ARG3) )
361 (#$implies (#$and (#$genlPreds ?PRED ?GENL-PRED) (?PRED ?ARG1 ?ARG2) ) (?GENL-PRED ?ARG1 ?ARG2 ) )
;;; #$genls
362 (#$isa #$genls #$DefaultMonotonicPredicate )
363 (#$isa #$genls #$ReflexiveBinaryPredicate )
364 (#$isa #$genls #$TransitiveBinaryPredicate )
365 (#$arity #$genls 2 )
366 (#$arg1Isa #$genls #$Collection )
367 (#$arg2Isa #$genls #$Collection )
368 (#$implies (#$and (#$isa ?OBJ ?SUBSET ) (#$genls ?SUBSET ?SUPERSET ) ) (#$isa ?OBJ ?SUPERSET ) )
369 (#$implies (#$resultgenl ?FUNC ?COLL ) (#$genls (?FUNC ?ARG1 ?ARG2 ?ARG3 ?ARG4 ?ARG5 ) ?COLL ) )
370 (#$implies (#$resultgenl ?FUNC ?COLL ) (#$genls ( ?FUNC ?ARG1 ?ARG2 ?ARG3 ?ARG4 ) ?COLL ) )
371 (#$implies (#$resultgenl ?FUNC ?COLL) (#$genls (?FUNC ?ARG1 ?ARG2 ?ARG3) ?COLL ) )
372 (#$implies (#$resultgenl ?FUNC ?COLL) (#$genls (?FUNC ?ARG1 ?ARG2) ?COLL ) )
373 (#$implies (#$resultgenl ?FUNC ?COLL) (#$genls (?FUNC ?ARG1) ?COLL) )
;;; #$hasAttributes
374 (#$isa #$hasAttributes #$BinaryPredicate )
375 (#$arity #$hasAttributes 2)
376 (#$arg1Isa #$hasAttributes #$TemporalObject )
377 (#$arg2Isa #$hasAttributes #$AttributeValue )
378 (#$not (#$and (#$hasAttributes ?Z ?X ) (#$hasAttributes ?Z ?Y ) (#$negationAttribute ?X ?Y ) ) )
;;; #$holdsIn
379 (#$isa #$holdsIn #$BinaryPredicate)
380 (#$arity #$holdsIn 2)
381 (#$arg1Isa #$holdsIn #$TemporalObject )
382 (#$arg2Isa #$holdsIn #$CycFormula )
;;; #$implies
383 (#$isa #$implies #$Relationship )
384 (#$arity #$implies 2)
385 (#$arg2Isa #$implies #$CycFormula )
386 (#$arg1Isa #$implies #$CycFormula )
387 (#$resultIsa #$implies #$CycFormula )
;;; #$interArgIsa1-2
388 (#$isa #$interArgIsa1-2 #$TernaryPredicate)
389 (#$arity #$interArgIsa1-2 3)
390 (#$arg1Isa #$interArgIsa1-2 #$Predicate)
391 (#$arg2Isa #$interArgIsa1-2 #$Collection)
392 (#$arg3Isa #$interArgIsa1-2 #$Collection)
393 (#$implies (#$and (#$requiredArg1Pred ?COL-1 ?PRED ) (#$interArgIsa1-2 ?PRED ?COL-1 ?COL-2 ) ) (#$relationAllExists ?PRED ?COL-1 ?COL-2 ) )
394 (#$implies (#$and (#$isa ?INDEP-INS ?INDEP-COL) (?PRED ?INDEP-INS ?DEP-INS) (#$interArgIsa1-2 ?PRED ?INDEP-COL ?DEP-COL) ) (#$isa ?DEP-INS ?DEP-COL) )
;;; #$interArgIsa1-3
395 (#$isa #$interArgIsa1-3 #$TernaryPredicate)
396 (#$arity #$interArgIsa1-3 3)
397 (#$arg1Isa #$interArgIsa1-3 #$Predicate )
398 (#$arg2Isa #$interArgIsa1-3 #$Collection )
399 (#$arg3Isa #$interArgIsa1-3 #$Collection )
400 (#$implies (#$and (#$isa ?INDEP-INS ?INDEP-COL ) (#$interArgIsa1-3 ?PRED ?INDEP-COL ?DEP-COL ) (?PRED ?INDEP-INS ?ANY-ARG-2 ?DEP-INS) ) (#$isa ?DEP-INS ?DEP-COL ) )
;;; #$interArgIsa1-4
401 (#$isa #$interArgIsa1-4 #$TernaryPredicate)
402 (#$arity #$interArgIsa1-4 3 )
403 (#$arg1Isa #$interArgIsa1-4 #$Predicate )
404 (#$arg2Isa #$interArgIsa1-4 #$Collection )
405 (#$arg3Isa #$interArgIsa1-4 #$Collection) 406 (#$implies (#$and (#$isa ?INDEP-INS ?INDEP-COL) (#$interArgIsa1-4 ?PRED ?INDEP-COL ?DEP-COL) (?PRED ?INDEP-INS ?ANY-ARG-2 ?ANY-ARG-3 ?DEP-INS) ) (#$isa ?DEP-INS ?DEP-COL ) )
;;; #$interArgIsa1-5
407 (#$isa #$interArgIsa1-5 #$TernaryPredicate )
408 (#$arity #$interArgIsa1-5 3 )
409 (#$arg1Isa #$interArgIsa1-5 #$Predicate )
410 (#$arg2Isa #$interArgIsa1-5 #$Collection )
411 (#$arg3Isa #$interArgIsa1-5 #$Collection )
412 (#$implies (#$and (#$isa ?INDEP-INS ?INDEP-COL ) (#$interArgIsa1-5 ?PRED ?INDEP-COL ?DEP-COL ) ( ?PRED ?INDEP-INS ?ANY-ARG-2 ?ANY-ARG-3 ?ANY-ARG-4 ?DEP-INS ) ) (#$isa ?DEP-INS ?DEP-COL) )
;;; #$interArgIsa2-1
413 (#$isa #$interArgIsa2-1 #$TernaryPredicate )
414 (#$arity #$interArgIsa2-1 3 )
415 (#$arg1Isa #$interArgIsa2-1 #$Predicate )
416 (#$arg2Isa [[#$interArgIsa2-1 #$Collection) 417 (#$arg3Isa [[#$interArgIsa2-1 #$Collection) 418 (#$implies (#$and (#$isa ?INDEP-INS ?INDEP-COL ) (?PRED ?DEP-INS ?INDEP-INS ) (#$interArgIsa2-1 ?PRED ?INDEP-COL ?DEP-COL ) ) (#$isa ?DEP-INS ?DEP-COL) )
;;; #$interArgIsa2-3
419 (#$isa #$interArgIsa2-3 #$TernaryPredicate )
420 (#$arity #$interArgIsa2-3 3 )
421 (#$arg1Isa #$interArgIsa2-3 #$Predicate )
422 (#$arg2Isa #$interArgIsa2-3 #$Collection )
423 (#$arg3Isa #$interArgIsa2-3 #$Collection ) 424 (#$implies (#$and (#$isa ?INDEP-INS ?INDEP-COL ) (#$interArgIsa2-3 ?PRED ?INDEP-COL ?DEP-COL ) (?PRED ?ANY-ARG-1 ?INDEP-INS ?DEP-INS ) ) (#$isa ?DEP-INS ?DEP-COL ) )
;;; #$interArgIsa2-4
425 (#$isa #$interArgIsa2-4 #$TernaryPredicate )
426 (#$arity #$interArgIsa2-4 3 )
427 (#$arg1Isa #$interArgIsa2-4 #$Predicate )
428 (#$arg2Isa #$interArgIsa2-4 #$Collection )
429 (#$arg3Isa #$interArgIsa2-4 #$Collection ) 430 (#$implies (#$and (#$isa ?INDEP-INS ?INDEP-COL ) (#$interArgIsa2-4 ?PRED ?INDEP-COL ?DEP-COL ) (?PRED ?ANY-ARG-1 ?INDEP-INS ?ANY-ARG-3 ?DEP-INS ) ) (#$isa ?DEP-INS ?DEP-COL ) )
;;; #$interArgIsa2-5
431 (#$isa #$interArgIsa2-5 #$TernaryPredicate )
432 (#$arity #$interArgIsa2-5 3 )
433 (#$arg1Isa #$interArgIsa2-5 #$Predicate )
434 (#$arg2Isa #$interArgIsa2-5 #$Collection )
435 (#$arg3Isa #$interArgIsa2-5 #$Collection ) 436 (#$implies (#$and (#$isa ?INDEP-INS ?INDEP-COL ) (#$interArgIsa2-5 ?PRED ?INDEP-COL ?DEP-COL) (?PRED ?ANY-ARG-1 ?INDEP-INS ?ANY-ARG-3 ?ANY-ARG-4 ?DEP-INS ) ) (#$isa ?DEP-INS ?DEP-COL ) )
;;; #$interArgIsa3-1
437 (#$isa #$interArgIsa3-1 #$TernaryPredicate )
438 (#$arity #$interArgIsa3-1 3 )
439 (#$arg1Isa #$interArgIsa3-1 #$Predicate )
440 (#$arg2Isa #$interArgIsa3-1 #$Collection )
441 (#$arg3Isa #$interArgIsa3-1 #$Collection ) 442 (#$implies (#$and (#$isa ?INDEP-INS ?INDEP-COL ) (#$interArgIsa3-1 ?PRED ?INDEP-COL ?DEP-COL ) (?PRED ?DEP-INS ?ANY-ARG-2 ?INDEP-INS ) ) (#$isa ?DEP-INS ?DEP-COL ) )
;;; #$interArgIsa3-2
443 (#$isa #$interArgIsa3-2 #$TernaryPredicate )
444 (#$arity #$interArgIsa3-2 3 )
445 (#$arg1Isa #$interArgIsa3-2 #$Predicate )
446 (#$arg2Isa #$interArgIsa3-2 #$Collection)
447 (#$arg3Isa #$interArgIsa3-2 #$Collection )
448 (#$implies (#$and (#$isa ?INDEP-INS ?INDEP-COL ) (#$interArgIsa3-2 ?PRED ?INDEP-COL ?DEP-COL ) (?PRED ?ANY-ARG-1 ?DEP-INS ?INDEP-INS ) ) (#$isa ?DEP-INS ?DEP-COL) )
;;; #$interArgIsa3-4
449 (#$isa #$interArgIsa3-4 #$TernaryPredicate )
450 (#$arity #$interArgIsa3-4 3 )
451 (#$arg1Isa #$interArgIsa3-4 #$Predicate )
452 (#$arg2Isa #$interArgIsa3-4 #$Collection)
453 (#$arg3Isa #$interArgIsa3-4 #$Collection )
454 (#$implies (#$and (#$isa ?INDEP-INS ?INDEP-COL ) (#$interArgIsa3-4 ?PRED ?INDEP-COL ?DEP-COL ) (?PRED ?ANY-ARG-1 ?ANY-ARG-2 ?INDEP-INS ?DEP-INS ) ) (#$isa ?DEP-INS ?DEP-COL ) )
;;; #$interArgIsa3-5
455 (#$isa #$interArgIsa3-5 #$TernaryPredicate )
456 (#$arity #$interArgIsa3-5 3 )
457 (#$arg1Isa #$interArgIsa3-5 #$Predicate )
458 (#$arg2Isa #$interArgIsa3-5 #$Collection )
459 (#$arg3Isa #$interArgIsa3-5 #$Collection) 460 (#$implies (#$and (#$isa ?INDEP-INS ?INDEP-COL ) (#$interArgIsa3-5 ?PRED ?INDEP-COL ?DEP-COL ) (?PRED ?ANY-ARG-1 ?ANY-ARG-2 ?INDEP-INS ?ANY-ARG-4 ?DEP-INS ) ) (#$isa ?DEP-INS ?DEP-COL ) )
;;; #$interArgIsa4-1
461 (#$isa #$interArgIsa4-1 #$TernaryPredicate )
462 (#$arity #$interArgIsa4-1 3 )
463 (#$arg1Isa #$interArgIsa4-1 #$Predicate )
464 (#$arg2Isa #$interArgIsa4-1 #$Collection )
465 (#$arg3Isa #$interArgIsa4-1 #$Collection ) 466 (#$implies (#$and (#$isa ?INDEP-INS ?INDEP-COL ) (#$interArgIsa4-1 ?PRED ?INDEP-COL ?DEP-COL ) (?PRED ?DEP-INS ?ANY-ARG-2 ?ANY-ARG-3 ?INDEP-INS ) ) (#$isa ?DEP-INS ?DEP-COL ) )
;;; #$interArgIsa4-2
467 (#$isa #$interArgIsa4-2 #$TernaryPredicate )
468 (#$arity #$interArgIsa4-2 3 )
469 (#$arg1Isa #$interArgIsa4-2 #$Predicate )
470 (#$arg2Isa #$interArgIsa4-2 #$Collection )
471 (#$arg3Isa #$interArgIsa4-2 #$Collection ) 472 (#$implies (#$and (#$isa ?INDEP-INS ?INDEP-COL ) (#$interArgIsa4-2 ?PRED ?INDEP-COL ?DEP-COL ) (?PRED ?ANY-ARG-1 ?DEP-INS ?ANY-ARG-3 ?INDEP-INS ) ) (#$isa ?DEP-INS ?DEP-COL ) )
;;; #$interArgIsa4-3
473 (#$isa #$interArgIsa4-3 #$TernaryPredicate )
474 (#$arity #$interArgIsa4-3 3 )
475 (#$arg1Isa #$interArgIsa4-3 #$Predicate )
476 (#$arg2Isa #$interArgIsa4-3 #$Collection )
477 (#$arg3Isa #$interArgIsa4-3 #$Collection ) 478 (#$implies (#$and (#$isa ?INDEP-INS ?INDEP-COL ) (#$interArgIsa4-3 ?PRED ?INDEP-COL ?DEP-COL ) (?PRED ?ANY-ARG-1 ?ANY-ARG-2 ?DEP-INS ?INDEP-INS ) ) (#$isa ?DEP-INS ?DEP-COL ) )
;;; #$interArgIsa4-5
479 (#$isa #$interArgIsa4-5 #$TernaryPredicate )
480 (#$arity #$interArgIsa4-5 3 )
481 (#$arg1Isa #$interArgIsa4-5 #$Predicate )
482 (#$arg2Isa #$interArgIsa4-5 #$Collection )
483 (#$arg3Isa #$interArgIsa4-5 #$Collection ) 484 (#$implies (#$and (#$isa ?INDEP-INS ?INDEP-COL ) (#$interArgIsa4-5 ?PRED ?INDEP-COL ?DEP-COL ) (?PRED ?ANY-ARG-1 ?ANY-ARG-2 ?ANY-ARG-3 ?INDEP-INS ?DEP-INS ) ) (#$isa ?DEP-INS ?DEP-COL ) )
;;; #$interArgIsa5-1
485 (#$isa #$interArgIsa5-1 #$TernaryPredicate )
486 (#$arity #$interArgIsa5-1 3 )
487 (#$arg1Isa #$interArgIsa5-1 #$QuintaryPredicate )
488 (#$arg2Isa #$interArgIsa5-1 #$Collection )
489 (#$arg3Isa #$interArgIsa5-1 #$Collection ) 490 (#$implies (#$and (#$isa ?INDEP-INS ?INDEP-COL) (#$interArgIsa5-1 ?PRED ?INDEP-COL ?DEP-COL) (?PRED ?DEP-INS ?ANY-ARG-2 ?ANY-ARG-3 ?ANY-ARG-4 ?INDEP-INS ) ) (#$isa ?DEP-INS ?DEP-COL ) )
;;; #$interArgIsa5-2
491 (#$isa #$interArgIsa5-2 #$TernaryPredicate )
492 (#$arity #$interArgIsa5-2 3 )
493 (#$arg1Isa #$interArgIsa5-2 #$QuintaryPredicate )
494 (#$arg2Isa #$interArgIsa5-2 #$Collection)
495 (#$arg3Isa #$interArgIsa5-2 #$Collection)
496 (#$implies (#$and (#$isa ?INDEP-INS ?INDEP-COL ) (#$interArgIsa5-2 ?PRED ?INDEP-COL ?DEP-COL ) (?PRED ?ANY-ARG-1 ?DEP-INS ?ANY-ARG-3 ?ANY-ARG-4 ?INDEP-INS ) ) (#$isa ?DEP-INS ?DEP-COL ) )
;;; #$interArgIsa5-3
497 (#$isa #$interArgIsa5-3 #$TernaryPredicate )
498 (#$arity #$interArgIsa5-3 3 )
499 (#$arg1Isa #$interArgIsa5-3 #$QuintaryPredicate )
500 (#$arg2Isa #$interArgIsa5-3 #$Collection )
501 (#$arg3Isa #$interArgIsa5-3 #$Collection ) 502 (#$implies (#$and (#$isa ?INDEP-INS ?INDEP-COL ) (#$interArgIsa5-3 ?PRED ?INDEP-COL ?DEP-COL ) (?PRED ?ANY-ARG-1 ?ANY-ARG-2 ?DEP-INS ?ANY-ARG-4 ?INDEP-INS ) ) (#$isa ?DEP-INS ?DEP-COL ) )
;;; #$interArgIsa5-4
503 (#$isa #$interArgIsa5-4 #$TernaryPredicate )
504 (#$arity #$interArgIsa5-4 3)
505 (#$arg1Isa #$interArgIsa5-4 #$QuintaryPredicate )
506 (#$arg2Isa #$interArgIsa5-4 #$Collection )
507 (#$arg3Isa #$interArgIsa5-4 #$Collection) 508 (#$implies (#$and (#$isa ?INDEP-INS ?INDEP-COL ) (#$interArgIsa5-4 ?PRED ?INDEP-COL ?DEP-COL ) (?PRED ?ANY-ARG-1 ?ANY-ARG-2 ?ANY-ARG-3 ?DEP-INS ?INDEP-INS ) ) (#$isa ?DEP-INS ?DEP-COL ) )
;;; #$relationExistsAll
509 (#$isa #$relationExistsAll #$TernaryPredicate )
510 (#$arity #$relationExistsAll 3 )
511 (#$arg1Isa #$relationExistsAll #$BinaryPredicate )
512 (#$arg2Isa #$relationExistsAll #$Collection )
513 (#$arg3Isa #$relationExistsAll #$Collection )
;;; #$relationExistsCountAll
514 (#$isa #$relationExistsCountAll #$QuaternaryPredicate )
515 (#$arity #$relationExistsCountAll 4 )
516 (#$arg1Isa #$relationExistsCountAll #$BinaryPredicate )
517 (#$arg2Isa #$relationExistsCountAll #$Collection)
518 (#$arg3Isa #$relationExistsCountAll #$Collection)
519 (#$arg4Isa #$relationExistsCountAll #$NonNegativeInteger )
;;; #$isa
520 (#$isa #$isa #$DefaultMonotonicPredicate )
521 (#$isa #$isa #$BinaryPredicate )
522 (#$arity #$isa 2 )
523 (#$arg1Isa #$isa #$ReifiableTerm )
524 (#$arg2Isa #$isa #$Collection )
525 (#$implies ( #$resultIsa ?F ?COL ) ( #$isa (?F ?ARG1 ?ARG2 ?ARG3 ) ?COL ) ) 526 (#$implies (#$resultIsa ?F ?COL ) (#$isa (?F ?ARG1 ?ARG2 ) ?COL ) ) 527 (#$implies (#$resultIsa ?F ?COL) (#$isa (?F ?ARG1 ) ?COL ) )
;;; #$ist
528 (#$isa #$ist #$BinaryPredicate )
529 (#$arity #$ist 2 )
530 (#$arg1Isa #$ist #$Microtheory )
531 (#$arg2Isa #$ist #$CycFormula )
;;; #$lispDefun
532 (#$isa #$lispDefun #$BinaryPredicate )
533 (#$arity #$lispDefun 2 )
534 (#$arg1Isa #$lispDefun #$EvaluatableFunction )
535 (#$arg2Isa #$lispDefun #$CycSystemSymbol )
;;; #$minimizeExtent
536 (#$isa #$minimizeExtent #$UnaryPredicate )
537 (#$arity #$minimizeExtent 1 )
538 (#$arg1Isa #$minimizeExtent #$Predicate )
;;; #$mtInferenceFunction
539 (#$isa #$mtInferenceFunction #$BinaryPredicate )
540 (#$arity #$mtInferenceFunction 2 )
541 (#$arg1Isa #$mtInferenceFunction #$Microtheory )
542 (#$arg2Isa #$mtInferenceFunction #$CycSystemSymbol )
;;; #$myCreationTime
543 (#$isa #$myCreationTime #$BinaryPredicate )
544 (#$isa #$myCreationTime #$BookkeepingPredicate )
545 (#$arity #$myCreationTime 2 )
546 (#$arg1Isa #$myCreationTime #$Thing )
547 (#$arg2Isa #$myCreationTime #$PositiveInteger )
;;; #$myCreator
548 (#$isa #$myCreator #$BinaryPredicate )
549 (#$isa #$myCreator #$BookkeepingPredicate )
550 (#$arity #$myCreator 2)
551 (#$arg1Isa #$myCreator #$Thing )
552 (#$arg2Isa #$myCreator #$Cyclist )
;;; #$negationAttribute
553 (#$isa #$negationAttribute #$SymmetricBinaryPredicate )
554 (#$isa #$negationAttribute #$IrreflexiveBinaryPredicate )
555 (#$genlInverse #$negationAttribute #$negationAttribute )
556 (#$arity #$negationAttribute 2)
557 (#$arg1Isa #$negationAttribute #$AttributeValue )
558 (#$arg2Isa #$negationAttribute #$AttributeValue )
;;; #$negationInverse
559 (#$isa #$negationInverse #$SymmetricBinaryPredicate )
560 (#$isa #$negationInverse #$IrreflexiveBinaryPredicate )
561 (#$genlInverse #$negationInverse #$negationInverse )
562 (#$arity #$negationInverse 2 )
563 (#$arg1Isa #$negationInverse #$BinaryPredicate )
564 (#$arg2Isa #$negationInverse #$BinaryPredicate ) 565 (#$not (#$and (#$negationInverse ?GEN-PRED ?PRED) (?PRED ?ARG1 ?ARG2) (?GEN-PRED ?ARG2 ?ARG1) ) )
;;; #$negationPreds
566 (#$isa #$negationPreds #$SymmetricBinaryPredicate )
567 (#$genlInverse #$negationPreds #$negationPreds)
568 (#$arity #$negationPreds 2 )
569 (#$arg1Isa #$negationPreds #$Predicate )
570 (#$arg2Isa #$negationPreds #$Predicate ) 571 (#$not (#$and (?PRED ?ARG1) (?NEG-PRED ?ARG1) (#$negationPreds ?NEG-PRED ?PRED ) ) ) 572 (#$not (#$and (#$negationPreds ?NEG-PRED ?PRED) (?PRED ?ARG1 ?ARG2 ?ARG3 ?ARG4 ?ARG5) (?NEG-PRED ?ARG1 ?ARG2 ?ARG3 ?ARG4 ?ARG5) ) ) 573 (#$not (#$and (#$negationPreds ?NEG-PRED ?PRED) (?PRED ?ARG1 ?ARG2 ?ARG3 ?ARG4) (?NEG-PRED ?ARG1 ?ARG2 ?ARG3 ?ARG4 ) ) ) 574 (#$not (#$and (#$negationPreds ?NEG-PRED ?PRED) (?PRED ?ARG1 ?ARG2 ?ARG3) (?NEG-PRED ?ARG1 ?ARG2 ?ARG3) ) ) 575 (#$not (#$and (#$negationPreds ?NEG-PRED ?PRED) (?PRED ?ARG1 ?ARG2) (?NEG-PRED ?ARG1 ?ARG2) ) )
;;; #$not
576 (#$isa #$not #$Relationship )
577 (#$arity #$not 1 )
578 (#$arg1Isa #$not #$CycFormula )
579 (#$resultIsa #$not #$CycFormula )
;;; #$oldConstantName
580 (#$isa #$oldConstantName #$BinaryPredicate )
581 (#$arity #$oldConstantName 2 )
582 (#$arg1Isa #$oldConstantName #$Thing )
583 (#$arg2Isa #$oldConstantName #$CycSystemString )
;;; #$or
584 (#$isa #$or #$CommutativeRelation )
585 (#$isa #$or #$VariableArityRelation )
586 (#$argsIsa #$or #$CycFormula )
587 (#$resultIsa #$or #$CycFormula )
;;; #$relationAllExists
588 (#$isa #$relationAllExists #$TernaryPredicate )
589 (#$arity #$relationAllExists 3 )
590 (#$arg1Isa #$relationAllExists #$BinaryPredicate )
591 (#$arg2Isa #$relationAllExists #$Collection )
592 (#$arg3Isa #$relationAllExists #$Collection )
;;; #$relationAllExistsCount
593 (#$isa #$relationAllExistsCount #$QuaternaryPredicate )
594 (#$arity #$relationAllExistsCount 4 )
595 (#$arg1Isa #$relationAllExistsCount #$BinaryPredicate )
596 (#$arg2Isa #$relationAllExistsCount #$Collection )
597 (#$arg3Isa #$relationAllExistsCount #$Collection )
598 (#$arg4Isa #$relationAllExistsCount #$NonNegativeInteger )
;;; #$requiredArg1Pred
600 (#$isa #$requiredArg1Pred #$BinaryPredicate )
601 (#$arity #$requiredArg1Pred 2 )
602 (#$arg1Isa #$requiredArg1Pred #$Collection )
603 (#$arg2Isa #$requiredArg1Pred #$Predicate )
;;; #$requiredArg2Pred
604 (#$isa #$requiredArg2Pred #$BinaryPredicate )
605 (#$arity #$requiredArg2Pred 2 )
606 (#$arg1Isa #$requiredArg2Pred #$Collection )
607 (#$arg2Isa #$requiredArg2Pred #$Predicate )
;;; #$resultgenl
608 (#$isa #$resultgenl #$BinaryPredicate )
609 (#$arity #$resultGenl 2 )
610 (#$arg1Isa #$resultGenl #$CollectionDenotingFunction )
611 (#$arg2Isa #$resultGenl #$Collection )
;;; #$resultIsa
612 (#$isa #$resultIsa #$BinaryPredicate )
613 (#$arity #$resultIsa 2 )
614 (#$arg1Isa #$resultIsa #$Relationship )
615 (#$arg2Isa #$resultIsa #$Collection )
;;; #$satisfiesDescription
616 (#$isa #$satisfiesDescription #$TernaryPredicate )
617 (#$arity #$satisfiesDescription 3 )
618 (#$arg1Isa #$satisfiesDescription #$CycSystemList )
619 (#$arg2Isa #$satisfiesDescription #$CycSystemList )
620 (#$arg3Isa #$satisfiesDescription #$Microtheory )
;;; #$siblingDisjointExceptions
621 (#$isa #$siblingDisjointExceptions #$SymmetricBinaryPredicate )
622 (#$isa #$siblingDisjointExceptions #$IrreflexiveBinaryPredicate )
623 (#$genlInverse]] #$siblingDisjointExceptions #$siblingDisjointExceptions )
624 (#$arity #$siblingDisjointExceptions 2 )
625 (#$arg1Isa #$siblingDisjointExceptions #$Collection )
626 (#$arg2Isa #$siblingDisjointExceptions #$Collection ) 627 (#$implies (#$siblingDisjointExceptions ?C1 ?C2 ) (#$siblingDisjointExceptions ?C1 ?C2 ) )
;;; #$termOfUnit
628 (#$isa #$termOfUnit #$DefaultMonotonicPredicate )
629 (#$isa #$termOfUnit #$InferenceRelatedBookkeepingPredicate )
630 (#$isa #$termOfUnit #$BinaryPredicate )
631 (#$arity #$termOfUnit 2 )
632 (#$arg1Isa #$termOfUnit #$ReifiableTerm )
633 (#$arg2Isa #$termOfUnit #$CycSystemList )
;;; #$thereExistAtLeast
634 (#$isa #$thereExistAtLeast #$Relationship )
635 (#$arity #$thereExistAtLeast 3 )
636 (#$resultIsa #$thereExistAtLeast #$CycFormula )
637 (#$arg3Isa #$thereExistAtLeast #$CycFormula )
638 (#$arg2Isa #$thereExistAtLeast #$CycELVariable )
639 (#$arg1Isa #$thereExistAtLeast #$PositiveInteger )
;;; #$thereExistAtMost
640 (#$isa #$thereExistAtMost #$Relationship )
641 (#$arity #$thereExistAtMost 3 )
642 (#$resultIsa #$thereExistAtMost #$CycFormula )
643 (#$arg3Isa #$thereExistAtMost #$CycFormula )
644 (#$arg2Isa #$thereExistAtMost #$CycELVariable )
645 (#$arg1Isa #$thereExistAtMost #$PositiveInteger )
;;; #$thereExistExactly
646 (#$isa #$thereExistExactly #$Relationship )
647 (#$arity #$thereExistExactly 3 )
648 (#$resultIsa #$thereExistExactly #$CycFormula )
649 (#$arg3Isa #$thereExistExactly #$CycFormula )
650 (#$arg2Isa #$thereExistExactly #$CycELVariable )
651 (#$arg1Isa #$thereExistExactly #$PositiveInteger)
;;; #$thereExists
652 (#$isa #$thereExists #$Relationship )
653 (#$arity #$thereExists 2 )
654 (#$arg2Isa #$thereExists #$CycFormula )
655 (#$arg1Isa #$thereExists #$CycELVariable )
Appendix B: Remarks about MELD Implementations
As we said earlier, there are several ideas, algorithms, data structures, additional constraints and simplifications, etc. that are inevitable and desirable when one is actually implementing MELD. MELD is a declarative language, so these things are not part of MELD proper, and moreover are likely to evolve as computers evolve. Nevertheless, they have great pragmatic value.
Rather than ignoring this side entirely, we have collected here in this Appendix some of the important remarks about implementation/efficiciency issues.
For example, it is almost a certainty that each implementation of MELD will need to include some way to find, for each constant, all the assertions that mention that constant. A frame-like implementation of MELD will need to rapidly find assertions where a particular constant x is used as the first argument to a binary predicate -- that is, all the assertions of the form (p x y); this "bundle" of assertions can be thought of as the x frame.
Each MELD constant is typically assigned a unique ID number; this facilitates multiple isolated groups exchanging their MELD assertions from time to time, if they each are permitted to rename the terms whenever they wish. To disambiguate things for the reader, in most languages, it's proven useful to prefix each MELD constant with a unique character string, such as "#$" (read "hash-dollar"). E.g., #$isa, #$Collection, #$Thing. These #$ characters are sometimes omitted in documents describing MELD, as they are herein, and of course they may be omitted by certain interface tools. They tell the reader that a MELD constant is about to be read, as opposed to an internal program function name, etc.
Constant-Naming Strategies
The following conventions are "merely" stylistic; they won't cause errors if you violate them, but you may find that some efficiency or even some functionality is lost if you ignore them. For example, some interface tools may expect term names like USAirForce and "parse" them for display to the user as "US Air Force". If you name that constant USAIRFORCE, that feature of that interface tool would be unable to help. Here are a few of these stylistic conventions:
To avoid confusion, we strongly recommend that no one create two MELD constants that differ only in case, such as Bill and BILL
All MELD logical connective names (and, or, not, equivalent, implies) and quantifier names (thereExists, forAll, thereExistAtLeast,. . .) and predicate names (isa, genls, colorOfObject) generally begin with a lowercase letter (a to z), right after the . E.g., implies, and, colorOfObject, forAll.
All other constant names (i.e., any name for a constant that isn't a logical connective or a predicate or a quantifier) generally begin with an uppercase letter (A to Z) or digit (0-9) right after the .
E.g., 3Mcorporation, MotherFn, BillClinton, Canada.
Stylistically, each MELD constant name should be composed of one or more meaningful "words" or abbreviations in sequence, with no breaks except for dashes or underlines (e.g. isa, colorOfObject, USAirForce, and SportsCar). A sequence of numeric characters may count as a "word" (e.g., FrontOfficeOfThe700Club).
With the exception noted above for predicate/quantifier/connective names, each (non-numeric) "word" in a sequence should (for visual clarity) begin with a capital letter. An acronym or abbreviation may count as a "word", but all its characters will be the same case (e.g., lower case if the acronym begins the name of a predicate constant; otherwise uppercase, such as avgHeight and IBMHeadquarters).
Hyphens are stylistically used to set off parts of names which restrict or refine the meaning of the name, as in Fruit-TheWord or Horse-Domesticated.
If two constants are closely related, it's often a good mnemonic to try to give them names which are alphabetically proximal. Why aspire to this? Some MELD interface tools make it easier to search for all constants whose name begins with a certain string of characters, or which contain a certain string, and it's easier to find all constants having to do with horses if they have been given names like Horse-Domesticated and Horse-Wild than if they have been given names like DomesticatedHorse and WildEquine.
When naming a constant, it's wise to assign a name that distinguishes the denoted concept from other concepts it might get confused with. So "Bow" would be a terrible name for a constant.
Instead, names like "Bow-BoatPart", "BowTheWeapon", "Bowing-BodyMovement" should be used, depending on the underlying concept denoted.
Sometimes it is possible to take this principle of specificity in names to an extreme, and attempt to embody the whole meaning of the constant in its name. This is discouraged.
For example, one might be tempted to give the constant physicalParts the name "distinctIdentifiablePhysicalParts", but it is better to leave the name a bit terser since it isn't easily confused with some other concept, and put the additional information in the constant documentation. Extremely long constant names make for lots of unnecessary typing, lots of typos, and lots of confusion because many terms will start out and end the same way. But extremely short constant names baffle the human reader and promote knowledge entry errors.
Variable-Naming Strategies
By convention, variables consist of all upper-case characters and numerals, and start with a letter of the alphabet (A-Z).
In formulas in which only one variable is used, it is common to use a single-letter variable, such as "?X". However, when a formula contains more than one variable, it will be much more readable if you give the variables mnemonic names. This is of course just a stylistic convention, a guideline, but one which you will be glad you -- and others -- adhered to.
Here's an example:
(#$implies (#$and (#$isa ?TRANSFER #$TransferringPossession ) (#$fromLocation ?TRANSFER ?FROM) ) (#$isa ?FROM #$SocialBeing) ) "The from location in a possession transfer is a social being."
Conventions for permitting/repairing unbound variables in formulas
Following a convention that has shown itself to be extremely useful for almost a century, if an unbound variable appears in a MELD formula, it is always assumed to be universally quantified. So, e.g., if this ill-formed formula were entered into a MELD interface that says
(#$implies (#$owns #$Fred ?X ) (#$objectFoundInLocation ?X #$FredsHouse) )
the interface should probably just automatically expand it into the following well-formed formula:
(#$forAll ?X (#$implies (#$owns #$Fred ?X) (#$objectFoundInLocation ?X #$FredsHouse) ) )
Since the former is easier to write and read, it is almost always preferred in practice, and you will rarely see a forAll while browsing the HPKB MELD IKB or Cyc KB (unless you use a browsing tool that reinserts them, just as the MELD inference engines themselves must.)
Warning: Uunbound variables which appear only in the consequent of a conditional, and not in the antecedent, may have drastic and undesired consequences.
Take, for example, the following:
(#$implies (#$owns #$Fred ?WHATEBER ) (#$objectFoundInLocation ?WHATEVER #$FredsHouse ) )
Because of the typo, the variable ?WHATEVER will range over the entire MELD ontology. In other words, the assertion above states that as long as Fred owns even one thing, then everything in the universe is located in FredsHouse--probably not what we -- or Fred-- would have wanted.
Note that this convention, interpreting all variables not explicitly bound as being universally quantified, treats those variables as having universal quantifiers at the beginning (left) of the formula, with formula-wide scope..
For example,
(#$lovesFact #$Mary (#$implies (#$isa ?W #$FemalePerson) (#$loves ?W #$Doug) ) )
is expanded to:
(#$forAll ?W (#$lovesFact #$Mary (#$implies (#$isa ?W #$FemalePerson) (#$loves ?W #$Doug) ) ) )
which says that when any female person loves Doug, Mary loves it;
it does not expand to:
(#$lovesFact #$Mary (#$forAll ?W (#$implies (#$isa ?W #$FemalePerson) (#$loves ?W #$Doug) ) ) )
which says that Mary loves the fact that all female people love Doug.
To say the latter, you need to put the forAll quantifier in explicitly parenthesized so as to indicate its scope.
In cases of nested mixed universal/existential quantifiers, it may be necessary to state the (non-outermost) forAll quantifiers explicitly, in order to capture the correct meaning of the formula.
I.e., clearly
(#$thereExists x (#$forAll y (P x y) )
is not the same thing as
(#$forAll y (#$thereExists x (P x y) ) )
Assertions
In each implementation of MELD, a formula will have to be represented somewhere/somehow in a data structure (e.g., as a string in an array called AXIOMS.)
A MELD KB will contain many formulae, hence the implemented "image" on the computer will contain just as many of these corresponding assertion structures. I.e., when a formula is successfully asserted into the KB, it is stored as an assertion. The details of this will vary from one MELD implementation to another, but here is an important set of information which, while it could be asserted and stored as a set of half a dozen separate formulae, really all fits together and should probably be (at least conceptually thought of as being) stored in each assertion data structure:
(( Assertion formula microtheory truth-value direction probability fuzziness support bookkeeping ))
where "formula" is the actual MELD Formula, and "microtheory" is the specific microtheory (context) in the KB in which the formula is being asserted to hold. See below for a more detailed explanation ofmicrotheories. The rest of the fields correspond to other various sorts of meta-assertions about the formula and how it is to be used. To wit:
formula --- the actual MELD formula
microtheory --- the context in which the formula is being asserted to hold. See Microtheories, above.
truth-value --- the truth value level at which that formula holds in that microtheory (monotonically true, default true, unknown, default false, or monotonically false); "unknown" generally means there are incommensurable pro/con arguments about that formula's truth. See Truth Values, above.
direction --- should the system try to maintain this assertion in a forward direction, "running the rule" at every possible opportunity? For further information about this, see Directions, below.
a (Bayesian) probability --- following recent thinking in this regard, this may turn out to be more than just one single number For further information about this, see Probability, above.
a fuzzy value --- following recent thinking in fuzzy truth and fuzzy probability. See Fuzzy Values, above.
support --- the justification; a set of pro/con arguments and the results of (trying to) compare them. For more details, see Support, above.
bookkeeping --- various data about who asserted this, what precise date and time, whether this subsumes/is subsumed by then-extant assertions in that KB, etc. This may also be the point of departure into some proprietary efficient-indexing scheme for assertions, should the implementer have such a thing.
Directions
Direction is a value associated with every assertion which determines when inference involving that assertion should be performed. There are two possible values for direction: forward and backward.
We could define predicates to specify the direction of each assertion, but in practice each MELD implementation and interface will most likely have some more efficient "in-line" way of tagging each assertion as it is made, for this "bit."
Inference involving assertions with direction forward is performed at assert time (that is, when a new assertion is added to the KB), while inference involving assertions with direction backward is postponed until a query occurs and that query allows backward inference.
Caution: Only in very special cases should rules have direction forward, lest an infinite regress be accidentally initiated (and, as we learned from Capt. Kirk, this leads to machines exploding in short order.)
These are the only 2 directions required by the MELD standard. However, there can be other directions besides these two, for particular MELD implementations. One useful direction that Cyc had way back in the mid-1980's, e.g., was EventuallyForward.
This meant "propagate it in a forward direction, but not right now, since I'm busy working." For each idiosyncratic Direction, there must be a translation of it into either Forward or Backward; i.e., if one wanted to run a MELD KB composed in one implementation that used EventuallyForward,. . . in another MELD implementation that only supported Backward and Forward.
In this particular example, EventuallyForward might translate to Forward. By default, it's safer to translate these idiosyncratic Directions to Backward.
Canonicalization of Assertions
People writing assertions for entry into a MELD KB will express their axioms in many ways; often, the very same axiom will have dozens of nearly-equally-good, natural-sounding, terse ways of expressing it (and of course an infinite number of logically equivalent but less-good ways besides.)
One important job of any MELD implementation is to tell when an assertion is already asserted, or redundant with one(s) that has/have already been asserted, or is inconsistent with one(s) that has/have already been asserted.
In general, this is a provably undecidable tasks. Tough. Pragmatically, what the users want and need and will accept is a correct but incomplete (i.e., resource-limited, heuristically-guided) canonicalizer. To say that that function is correct we mean that it won't claim P and Q are equivalent if indeed they are not. To say that the canonicalizer is incomplete means that it will sometimes fail to realize that P and Q are indeed equivalent even though they are. What's important is that it does indeed work on the common cases, that it work efficiently enough for the applications which the MELD axioms are being used for, etc.
Skolemization
To illustrate Canonicalization, and to tie this in with our preceding discussion of Quantification, consider that MELD users will assert axioms to the KB which use thereExists quite frequently, and somehow each implementation of MELD must decide how best to internally represent such assertions, so that it can have the best possible chance of noticing already-entered axioms, redundant ones, inconsistent ones, etc.
We present here one sample idea; think of it as a glimpse at how the internals of Cyc happens to work, circa mid-1990's. It is just one possible way of implementing this.
Once existential assertions are entered into the Cyc KB, occurences of thereExists are automatically converted into Skolem functions.. Thus, an assertion which was entered as:
([[#$implies
(#$isa ?A #$Animal)
(#$thereExists ?M
(#$and (#$mother ?A ?M)
('#$isa ?M #$FemaleAnimal)') ) )
is canonicalized into four separate, smaller assertions, plus the definition of brand new MELD function called SKF. . ., as follows:
(#$isa #$SKF-8675309 #SkolemFunction )
(#arity #SKF-8675309 1) ('#$implies (#$isa ?A $#Animal ) (mother ?A (#$SKF-8675309 ?A ) ) ) (#$implies (#$isa ?A #$Animal ) (#$isa (#$SKF-8675309 ?A ) #$FemaleAnimal ) )
Intuitively, you can think of that new MELD function SKF-8675309 as calculating the mother of its argument. These new functions start out named SKF-. . . because they are Skolem functions. To reiterate: your implementation of MELD may or may not create these functions. As a stylistic recommendation, we strongly suggest that even if you do "split up" an asserted axiom into several, for any reason (such as the skolemization just did, or because the top-level connective was and, or for any other reason) that a record is kept of the fact that that set of assertions was entered together as one single assertion; further, we suggest that each MELD implementation maintain records of who asserted each axiom, when, the exact way they phrased the axiom, even the particular variable names they chose. Many useful user interface tools can make effective use of such information.
Reifiable vs. Non-Reifiable Functions
This is once again a digression to a MELD implementation level issue. In theory, any MELD function can be used to construct NATs, and those NATs can be used where a constant term or variable would otherwise appear.
However, we have found it highly cost-effective to have and use a distinction which is akin to "declaring" certain functions as having their NATs treated more like reified (named) constants.
In Cyc, e.g., many of the functions (that is, instances of the Collection Function) in its ontology are also asserted to be instances of #$ReifiableFunction, a subset of Function. Each time an instance of ReifiableFunction is used with a new set of arguments to build a NAT, that NAT is instantly reified, that is, preserved in the MELD ontology as a constant. Constants which are reified NATs may or may not immediately inform the asserter of what the name is, or accept a name from them; this is up to the particular user interfaces and application interfaces. It should be the case that a natural-sounding name, of the user's choice, should be assertable later on, just as the user should be given the facility for renaming practically any other constant he/she chooses to rename.
In Cyc, when a new reified NAT-constant is first created, the Cyc implementation of MELD automatically sets up the following correspondence
(#termOfUnit NAT-CONSTANT NAT-EXPRESSION)
where NAT-CONSTANT is the automatically-created constant (probably having some awful name, just like those awful Skolem Function names discussed above) and NAT-EXPRESSION is the non-atomic term that can be used to refer to it.
In the current Cyc Web-based interface tool, such an assertion might look like this:
('termOfUnit (GovernmentFn Canada) (GovernmentFn Canada)')
It looks like the first and second arguments are the same, but that's because, in lieu of a proper constant name for the reified NAT-constant, the system uses the NAT expression as a print name. If you rename that NAT later, say to CanadianGovt, then the assertion would appear more like you'd expect:
(#$termOfUnit ([[#$GovernmentFn Canada) )
Also, one could adjust the interface tool to make the internal ugly name appear even before that renaming, so one might see
('termOfUnit NAT-70594892 (GovernmentFn Canada)')
If you look very carefully at any termOfUnit assertion in the current Cyc web-based interface tool, you will see that the opening parenthesis of ARG1 is a followable hyperlink (depending on the web-browser you use, it may be underlined, or in a different color, from most of the left parentheses on your screen); notice that the opening parenthesis of ARG2 is just opaque text, not a followable hyperlink. Clicking on the opening parenthesis of a NAT expression will display the page for the reified NAT-constant the expression denotes.
A reified NAT can be explicitly identified with an already-existing constant by using the predicate termOfUnit:
(#$termOfUnit #$TheYear1996 (#$YearFn 1996) ) (#$termOfUnit #$Apple (#$FruitFn #$AppleTree) )
When a NAT is identified with a constant using #$termOfUnit, the two are asserted to be de dicto equivalent. Someone may know about apples, and apple trees, and the bearing of fruit by trees, without knowing that apples are the fruit that comes from apple trees. Of course if they know those concepts using those very English words, it's hard to imagine they don't know where apples come from.
Skolem functions are reifiable.
Earlier, we said that almost all functions in the MELD ontology are reifiable. Why wouldn't they all be? Non-reifiable functions mostly consist of arithmetic and other mathematical functions like PlusFn. Just because we use a NAT like (PlusFn 59 64) doesn't mean we want to add to the KB a full-fledged constant term like TheNumber123, denoting the number 123. If we want to talk about the number 123, we'll just refer to it directly.
Quantifying into NATs
It is possible in MELD to write rules which involve quantifying into a NAT, that is, using a NAT which has a variable as one of its arguments.
For example, suppose we want to say that a previously-owned car is a used car, a previously-owned TV is a used TV, etc. I.e., we want to state the general relationship between the PreviouslyOwnedFn function and the Used attribute. PreviouslyOwnedFn is a function which, when applied to a collection representing a type of product, returns a new collection which is those which are already owned and "in service"; i.e., not brand new. Thus (PreviouslyOwnedFn Car) is the collection of all cars that are not brand new. The Used attribute can be asserted to be true about any particular individual product, and it means that that particular item is not brand new.
Here is the axiom that interrelates PreviouslyOwnedFn and Used:
(forAll ?POSSESSION-TYPE
([[#$implies
('#$isa ?X (PreviouslyOwnedFn ?POSSESSION-TYPE)')
(hasAttributes ?X Used)')')
When ?POSSESSION-TYPE is bound to Car, for example, this axiom says that each member of the set of previously-owned cars is Used.
For efficiency's sake, some implementations of MELD may require that you not quantify into a NAT unless it is built on an instance of #$ReifiableFunction.
This does not limit the generality of the mechanism, since any MELD function of interest can be declared to be reifiable; it is just a sort of "declaration" which might speed up some MELD inference engines.
Appendix C: BNF Grammar for MELD
This BNF can be used to check for syntactic well-formedness of a MELD formula, and -- coupled with the 650 formulas above in Appendix A, -- to check a MELD formula for semantic well-formedness as well.
Assume the following Terminals (token-level non-terminals)
<Character>
<String>
<Number>
<Symbol>
<Variable>
Assume the following MELD data object:
<Constant>
The empty expansion is:
<epsilon>
;;;;;;;;;;;;;;;;;;;;;;;;
;; Syntactic Constraints
;;;;;;;;;;;;;;;;;;;;;;;;
<Formula> ::= #$True
| #$False
| <Variable>
| <Literal>
| <NotForm>
| <AndForm>
| <OrForm>
| <XorForm>
| <ImpForm>
| <EquivForm>
| <UnivForm>
| <ExistForm>
| <ExistExactForm>
| <ExistUBoundForm>
| <ExistLBoundForm>
<Formula-Seq> ::= <Formula> <Formula-Seq>
| . <Variable>
| <epsilon>
<NotForm> ::= ( #$not <Formula> )
<AndForm> ::= ( #$and <Formula-Seq> )
<OrForm> ::= ( #$or <Formula-Seq> )
<XorForm> ::= ( #$xor <Formula> <Formula> )
<ImpForm> ::= ( #$implies <Formula> <Formula> )
<EquivForm> ::= ( #$equivalent <Formula> <Formula> )
<UnivForm> ::= ( #$forAll <Variable> <Formula> )
<ExistForm> ::= ( #$thereExists <Variable> <Formula> )
<ExistExactForm> ::= ( #$thereExistExactly <1stOrderTerm> <Variable> <Formula> )
<ExistUBoundForm> ::= ( #$thereExistAtMost <1stOrderTerm> <Variable> <Formula> )
<ExistLBoundForm> ::= ( #$thereExistAtLeast <1stOrderTerm> <Variable> <Formula> )
<Literal> ::= <AtomicFormula>
| ( #$not <AtomicFormula> )
<AtomicFormula> ::= ( <Predicate> <Argument-Seq> )
<Argument-Seq> ::= <2ndOrderTerm> <Argument-Seq>
| . <Variable>
| <epsilon>
<Predicate> ::= <Rep1stOrderTerm>
<FunctionExp> ::= ( <Function> <Argument-Seq> )
<Function> ::= <Rep1stOrderTerm>
<2ndOrderTerm> ::= <1stOrderTerm>
| <Formula>
<1stOrderTerm> ::= <Rep1stOrderTerm>
| <PrimitiveTerm>
<Rep1stOrderTerm> ::= <Constant>
| <FunctionExp>
| <Variable>
<PrimitiveTerm> ::= <Character>
| <String>
| <Number>
| <Symbol>
| <Variable>
;;;;;;;;;;;;;;;;;;;;;;;
;; Semantic Constraints
;;;;;;;;;;;;;;;;;;;;;;;
For <ExistExactForm> :
1st arg must denote a positive integer
For <ExistUBoundForm> :
1st arg must denote a positive integer
For <ExistLBoundForm> :
1st arg must denote a positive integer
For <Function> :
when <Function> is ground
(#$isa <Function> #$NonPredicateFunction) must be true
For <Predicate> :
when <Predicate> is ground
(#$isa <Predicate> #$Predicate) must be true
Relation Arity Constraints:
For <FunctionExp> :
when <Function> is ground
either
(#$isa <Function> #$VariableArityRelation)
or
(#$arity <Function> <N>)
and
<N> is a non-negative integer
and
if <Argument-Seq> is terminated by . <Variable>
the number of <2ndOrderTerm>s in <Argument-Seq>
must be less than or equal to <N>
else the number of <2ndOrderTerm>s in <Argument-Seq>
must be equal to <N>
For <AtomicFormula> :
when <Predicate> is ground
either
(#$isa <Predicate> #$VariableArityRelation)
or
(#$arity <Predicate> <N>)
and
<N> is a non-negative integer
and
if <Argument-Seq> is terminated by . <Variable>
the number of <2ndOrderTerm>s in <Argument-Seq>
must be less than or equal to <N>
else the number of <2ndOrderTerm>s in <Argument-Seq>
must be equal to <N>
Relation Argument Constraints:
For <FunctionExp> :
each term in <Argument-Seq> must satisfy all applicable arg constraints
(e.g., #$arg1Isa, #$interArgIsa2-1, ...)
or <AtomicFormula> :
each term in <Argument-Seq> must satisfy all applicable arg constraints
(e.g., #$arg1Isa, #$interArgIsa2-1, ...)
Footnotes
Why does the "M" in "MELD" stand for "Moderately" instead of "Most"? Because MELD intentionally omits some potential language features which, while they add to expressive power, are so costly to implement and rare and unwieldy to use that we feel they are just not cost-effective to include at this time (for example, quantification over quantifiers.)
As human beings, do we have complete definitions of most of the words and the concepts we use in our daily lives? Our notion of practically any concept (pet, vehicle, jumping, fun, white collar workers,. . .) is in effect the set of statements we believe about that concept -- no more and no less. Fortunately, since most of us share most of the same beliefs about most of the common concepts, we are able to communicate with each other with only an occasional miscommunication and need for clarification -- oh, around every third or fourth thing that's said to us!
Without sharing as much of that "content" as we do, we wouldn't even stand a chance to communicate effectively. Note that that point is even after we've agreed to speak English, follow English grammar, etc. That same principle underlies the notion of a fixed MELD KERNEL KB, for the HPKB IKB, and for the entire Cyc KB for that matter: a set of fundamental concepts and assertions about them, which are enough of a common core to permit knowledge sharing among those who abide by them. And that point is even after agreeing on having our programs "speak" MELD.
We require coverage (a mapping to) at least the printing ASCII character set, but MELD itself allows anything that is representable in Unicode, not just ASCII. This excludes, therefore, pure Hebrew, Cyrillic characters, Arabic characters, etc.
This "all possible" is where the theoretically "stronger higher-order" issues arise in formal logic; i.e., it is what makes MELD "strongly higher-order".
Go to Top Last Update: February 25, 1998 Copyright© 1997, 1998 Cycorp All rights reserved.
