Browsing Interface : Welcome guest : log in
|
Browsing Interface : Welcome guest : log in |
[
Home |
Graph |
LogLearn |
Editor |
]
KB:
Language:
Formal Language:
|
| domain |
| appearance as argument number 1 |
|
| (instance domain TernaryPredicate) | Merge.kif 201-201 | domain is an instance of ternary predicate |
| (domain domain 1 Relation) | Merge.kif 202-202 | The number 1 argument of domain is an instance of relation |
| (domain domain 2 PositiveInteger) | Merge.kif 203-203 | The number 2 argument of domain is an instance of positive integer |
| (domain domain 3 Class) | Merge.kif 204-204 | The number 3 argument of domain is an instance of class |
| (documentation domain EnglishLanguage "Provides a computationally and heuristically convenient mechanism for declaring the argument types of a given relation. The formula (domain ?REL ?INT ?CLASS) means that the ?INT'th element of each tuple in the relation ?REL must be an instance of ?CLASS. Specifying argument types is very helpful in maintaining ontologies. Representation systems can use these specifications to classify terms and check integrity constraints. If the restriction on the argument type of a Relation is not captured by a Class already defined in the ontology, one can specify a Class compositionally with the functions UnionFn, IntersectionFn, etc.") | Merge.kif 205-213 | The number 3 argument of domain is an instance of class |
| appearance as argument number 2 |
|
|
| (termFormat EnglishLanguage domain "domain") | domainEnglishFormat.kif 20112-20112 | |
| (termFormat ChineseTraditionalLanguage domain "域") | domainEnglishFormat.kif 20113-20113 | |
| (termFormat ChineseLanguage domain "域") | domainEnglishFormat.kif 20114-20114 | |
| (format EnglishLanguage domain "the number %2 argument of %1 is %n an instance of %3") | english_format.kif 296-296 |
| antecedent |
|
|
| (=> (and (subrelation ?PRED1 ?PRED2) (domain ?PRED2 ?NUMBER ?CLASS1)) (domain ?PRED1 ?NUMBER ?CLASS1)) |
Merge.kif 180-184 | If X is a subrelation of Y and the number Z argument of Y is an instance of W, then the number Z argument of X is an instance of W |
| (=> (and (domain ?REL ?NUMBER ?CLASS1) (domain ?REL ?NUMBER ?CLASS2)) (or (subclass ?CLASS1 ?CLASS2) (subclass ?CLASS2 ?CLASS1))) |
Merge.kif 215-221 | If the number X argument of Y is an instance of Z and the number X argument of Y is an instance of W, then Z is a subclass of W or W is a subclass of Z |
| (=> (and (domain ?REL1 ?NUMBER ?CLASS1) (domain ?REL2 ?NUMBER ?CLASS2) (disjoint ?CLASS1 ?CLASS2)) (disjointRelation ?REL1 ?REL2)) |
Merge.kif 411-416 | If the number X argument of Y is an instance of Z, the number X argument of W is an instance of V, and Z is disjoint from V, then Y and W are disjoint |
| (=> (and (domain ?REL ?NUMBER ?CLASS) (instance ?REL Predicate) (?REL @ROW)) (instance (ListOrderFn (ListFn @ROW) ?NUMBER) ?CLASS)) |
Merge.kif 3109-3114 | If the number X argument of Y is an instance of Z, Y is an instance of predicate, and Y @ROW, then V element of (@ROW) is an instance of Z |
| (=> (and (instance ?REL EconomicRelation) (domain ?REL 1 ?CLASS)) (subclass ?CLASS GeopoliticalArea)) |
Mid-level-ontology.kif 18523-18527 | If X is an instance of economic relation and the number 1 argument of X is an instance of Y, then Y is a subclass of geopolitical area |
| (=> (and (applicableRelation ?O ?R) (instance ?O ?OC) (domain ?R 1 ?DC)) (or (equal ?OC ?DC) (subclass ?OC ?DC))) |
Mid-level-ontology.kif 33896-33903 | If X can be an argument to Y, X is an instance of Z, and the number 1 argument of Y is an instance of W, then equal Z and W or Z is a subclass of W |
| consequent |
|
|
| (=> (and (subrelation ?PRED1 ?PRED2) (domain ?PRED2 ?NUMBER ?CLASS1)) (domain ?PRED1 ?NUMBER ?CLASS1)) |
Merge.kif 180-184 | If X is a subrelation of Y and the number Z argument of Y is an instance of W, then the number Z argument of X is an instance of W |
| (=> (instance ?FUN OneToOneFunction) (forall (?ARG1 ?ARG2) (=> (exists (?CLASS) (and (domain ?FUN 1 ?CLASS) (instance ?ARG1 ?CLASS) (instance ?ARG2 ?CLASS) (not (equal ?ARG1 ?ARG2)))) (not (equal (AssignmentFn ?FUN ?ARG1) (AssignmentFn ?FUN ?ARG2)))))) |
Merge.kif 3488-3498 | If X is an instance of one to one function, then For all Entities Y and Z: if there exists W such that the number 1 argument of X is an instance of W, Y is an instance of W, Z is an instance of W, equal Y, and Z, then equal X(Y) and X(Z) |
| (=> (instance ?FUNCTION AssociativeFunction) (forall (?INST1 ?INST2 ?INST3 ?CLASS) (=> (and (domain ?FUNCTION 1 ?CLASS) (instance ?INST1 ?CLASS) (instance ?INST2 ?CLASS) (instance ?INST3 ?CLASS)) (equal (AssignmentFn ?FUNCTION ?INST1 (AssignmentFn ?FUNCTION ?INST2 ?INST3)) (AssignmentFn ?FUNCTION (AssignmentFn ?FUNCTION ?INST1 ?INST2) ?INST3))))) |
Merge.kif 3531-3541 | If X is an instance of associative function, then For all Entities Y, Z, and W and Class V: if the number 1 argument of X is an instance of V, Y is an instance of V, Z is an instance of V, and W is an instance of V, then equal X(Y and X(Z and W)) and X(X(Y and Z) and W) |
| (=> (instance ?FUNCTION CommutativeFunction) (forall (?INST1 ?INST2 ?CLASS) (=> (and (domain ?FUNCTION 1 ?CLASS) (instance ?INST1 ?CLASS) (instance ?INST2 ?CLASS)) (equal (AssignmentFn ?FUNCTION ?INST1 ?INST2) (AssignmentFn ?FUNCTION ?INST2 ?INST1))))) |
Merge.kif 3551-3561 | If X is an instance of commutative function, then For all Entities Y and Z and Class W: if the number 1 argument of X is an instance of W, Y is an instance of W, and Z is an instance of W, then equal X(Y and Z) and X(Z and Y) |
| appearance as argument number 0 |
|
|
|