![]() |
appearance as argument number 1 |
![]() |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1991-1993 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3368-3371 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 625-627 | |
No TPTP formula. May not be expressible in strict first order. | pictureList.kif 11049-11049 | |
No TPTP formula. May not be expressible in strict first order. | pictureList.kif 10024-10024 | |
No TPTP formula. May not be expressible in strict first order. | pictureList.kif 11047-11047 | |
No TPTP formula. May not be expressible in strict first order. | pictureList.kif 11050-11050 | |
No TPTP formula. May not be expressible in strict first order. | pictureList.kif 11052-11052 | |
No TPTP formula. May not be expressible in strict first order. | pictureList.kif 11048-11048 | |
No TPTP formula. May not be expressible in strict first order. | pictureList.kif 11051-11051 | |
No TPTP formula. May not be expressible in strict first order. | pictureList.kif 11046-11046 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3366-3366 | Function is a subclass of inheritable relation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3365-3365 | Function is a subclass of single valued relation |
appearance as argument number 2 |
![]() |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 777-777 | Assignment is an instance of function |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4872-4872 | Greatest common divisor is an instance of function |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 575-575 | Latitude is an instance of function |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4957-4957 | Least common multiple is an instance of function |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2944-2944 | List is an instance of function |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 612-612 | Longitude is an instance of function |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3413-3413 | Binary function is a subclass of function |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3487-3487 | Continuous function is a subclass of function |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3476-3476 | Quaternary function is a subclass of function |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3465-3465 | Ternary function is a subclass of function |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3373-3373 | Unary function is a subclass of function |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 916-916 | Unary function is a subclass of function |
No TPTP formula. May not be expressible in strict first order. | english_format.kif 1039-1039 | Unary function is a subclass of function |
No TPTP formula. May not be expressible in strict first order. | french_format.kif 592-592 | Unary function is a subclass of function |
No TPTP formula. May not be expressible in strict first order. | terms-hindi.txt 122-122 | Unary function is a subclass of function |
No TPTP formula. May not be expressible in strict first order. | terms-it.txt 125-125 | Unary function is a subclass of function |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2277-2277 | Unary function is a subclass of function |
No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 544-544 | Unary function is a subclass of function |
No TPTP formula. May not be expressible in strict first order. | terms-cb.txt 127-127 | Unary function is a subclass of function |
No TPTP formula. May not be expressible in strict first order. | terms-cz.txt 159-159 | Unary function is a subclass of function |
No TPTP formula. May not be expressible in strict first order. | terms-de.txt 418-418 | Unary function is a subclass of function |
No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 613-613 | Unary function is a subclass of function |
No TPTP formula. May not be expressible in strict first order. | terms-tg.txt 126-126 | Unary function is a subclass of function |
appearance as argument number 3 |
![]() |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 779-779 | The number 1 argument of assignment is an instance of function |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3589-3589 | The number 1 argument of closed on is an instance of function |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 300-300 | The number 1 argument of range is an instance of function |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 327-327 | The number 1 argument of range subclass is an instance of function |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2173-2173 | Relation is exhaustively partitioned into predicate and function |
![]() |
![]() |