![]() |
![]() ![]() ![]()
|
![]() |
|
appearance as argument number 1 |
![]() |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1831-1832 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2246-2248 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 451-452 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2244-2244 | Binary relation is a subclass of inheritable relation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2243-2243 | Binary relation is a subclass of relation |
appearance as argument number 2 |
![]() |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2171-2172 | 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. | MilitaryDevices.kif 249-249 | angle of fire is an instance of binary relation |
No TPTP formula. May not be expressible in strict first order. | VirusProteinAndCellPart.kif 255-255 | catalyst is an instance of binary relation |
No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 726-726 | device OS is an instance of binary relation |
No TPTP formula. May not be expressible in strict first order. | QoSontology.kif 1130-1130 | hardware type is an instance of binary relation |
No TPTP formula. May not be expressible in strict first order. | QoSontology.kif 2201-2201 | has account is an instance of binary relation |
No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 4414-4414 | recovery key is an instance of binary relation |
No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 3857-3857 | software version is an instance of binary relation |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31497-31497 | suffers is an instance of binary relation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2303-2303 | Antisymmetric relation is a subclass of binary relation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3494-3494 | Binary predicate is a subclass of binary relation |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 18287-18287 | Economic relation is a subclass of binary relation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2360-2360 | Intransitive relation is a subclass of binary relation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2260-2260 | Irreflexive relation is a subclass of binary relation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2250-2250 | Reflexive relation is a subclass of binary relation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2271-2271 | Symmetric relation is a subclass of binary relation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2344-2344 | Transitive relation is a subclass of binary relation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2321-2321 | Trichotomizing relation is a subclass of binary relation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3374-3374 | Unary function is a subclass of binary relation |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 892-892 | Unary function is a subclass of binary relation |
No TPTP formula. May not be expressible in strict first order. | english_format.kif 986-986 | Unary function is a subclass of binary relation |
No TPTP formula. May not be expressible in strict first order. | french_format.kif 568-568 | Unary function is a subclass of binary relation |
No TPTP formula. May not be expressible in strict first order. | terms-hindi.txt 98-98 | Unary function is a subclass of binary relation |
No TPTP formula. May not be expressible in strict first order. | terms-it.txt 101-101 | Unary function is a subclass of binary relation |
Display limited to 25 items. Show next 25 | ||
Display limited to 25 items. Show next 25 |
appearance as argument number 3 |
![]() |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3720-3720 | The number 1 argument of equivalence relation on is an instance of binary relation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 111-111 | The number 1 argument of inverse is an instance of binary relation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 112-112 | The number 2 argument of inverse is an instance of binary relation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3657-3657 | The number 1 argument of partial ordering on is an instance of binary relation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3618-3618 | The number 1 argument of reflexive on is an instance of binary relation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3674-3674 | The number 1 argument of total ordering on is an instance of binary relation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3696-3696 | The number 1 argument of trichotomizing on is an instance of binary relation |
![]() |
![]() |