HourFn |
appearance as argument number 1 |
![]() |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 2764-2768 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8582-8588 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8578-8578 | The number 1 argument of hour is an instance of nonnegative integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8579-8579 | The number 2 argument of hour is a subclass of day |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8576-8576 | Hour is an instance of binary function |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8577-8577 | Hour is an instance of partial valued relation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8575-8575 | Hour is an instance of temporal relation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8580-8580 | The values returned by hour are subclasses of hour |
appearance as argument number 2 |
![]() |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 471-471 | |
No TPTP formula. May not be expressible in strict first order. | english_format.kif 477-477 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 9306-9306 | Hour is internally related to hour |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 28693-28693 | |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 472-472 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 28692-28692 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 28691-28691 |
antecedent |
![]() |
consequent |
![]() |
statement |
![]() |
No TPTP formula. May not be expressible in strict first order. | QoSontology.kif 2143-2143 | Unix epoch is equal to the second 0 |
![]() |
![]() |