|
|
   Relation
|
|
|
| appearance as argument number 1 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2073-2074 | 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 2078-2082 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2075-2075 | Relation is exhaustively partitioned into predicate and function |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2076-2076 | 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 2072-2072 | Relation is a subclass of abstract |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2144-2144 | Binary relation is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2464-2464 | Inheritable relation is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2577-2577 | Intentional relation 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 2135-2135 | Partial valued relation is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3222-3222 | Predicate is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2470-2470 | Probability relation is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2755-2755 | Quaternary relation is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2762-2762 | Quintary relation is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3414-3414 | Relation extended to quantities is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2089-2089 | Single valued relation is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2562-2562 | Spatial relation is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2569-2569 | Temporal relation is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2748-2748 | Ternary relation is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2107-2107 | Total valued relation is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3403-3403 | 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 412-412 | 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 413-413 | 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 207-207 | The number 1 argument of domain is an instance of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 229-229 | 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 170-170 | The number 1 argument of subrelation is an instance of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 171-171 | The number 2 argument of subrelation is an instance of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 361-361 | 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 1579-1579 | Abstract is disjointly decomposed into quantity, attribute, set or class, relation, proposition, and list |
| consequent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2116-2133 | 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
|
|
|
|