|
|
   Relation
|
|
|
| appearance as argument number 1 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2068-2069 | Relation is disjointly decomposed into binary relation, ternary relation, quaternary relation, quintary relation, and variable arity relation |
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1816-1819 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2072-2077 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2069-2069 | Relation is exhaustively partitioned into predicate, function, and list |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2070-2070 | Relation is exhaustively partitioned into total valued relation and partial valued relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2067-2067 | Relation is a subclass of abstract |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2139-2139 | Binary relation is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2459-2459 | Inheritable relation is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2572-2572 | Intentional relation is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2764-2764 | List is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 961-961 | PPP based economic valuation is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2130-2130 | Partial valued relation is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3217-3217 | Predicate is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2465-2465 | Probability relation is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2750-2750 | Quaternary relation is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2757-2757 | Quintary relation is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3409-3409 | Relation extended to quantities is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2084-2084 | Single valued relation is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2557-2557 | Spatial relation is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2564-2564 | Temporal relation is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2743-2743 | Ternary relation is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2102-2102 | Total valued relation is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3398-3398 | Variable arity relation is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 888-888 | |
| No TPTP formula. May not be expressible in strict first order. | english_format.kif 983-983 |
| appearance as argument number 3 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 411-411 | The number 1 argument of disjoint relation is an instance of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 412-412 | The number 2 argument of disjoint relation is an instance of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 206-206 | The number 1 argument of domain is an instance of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 228-228 | The number 1 argument of domain subclass is an instance of relation |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 2071-2071 | The number 1 argument of exactCardinality is an instance of relation |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 2189-2189 | The number 1 argument of maxCardinality is an instance of relation |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 2153-2153 | The number 1 argument of minCardinality is an instance of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 169-169 | The number 1 argument of subrelation is an instance of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 170-170 | The number 2 argument of subrelation is an instance of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 360-360 | The number 1 argument of valence is an instance of relation |
| appearance as argument number 5 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1574-1574 | Abstract is disjointly decomposed into quantity, attribute, set or class, relation, and proposition |
| consequent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2111-2128 | A relation is an instance of total valued relation and the relation is an instance of predicate if and only if there exists a positive integer such that the relation is an instance of relation and the relation %&has the positive integer argument(s) and
|
|
|
|