AbsoluteValueFn |
appearance as argument number 1 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 2224-2225 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4765-4766 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 888-889 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4762-4762 | O argumento numero 1 de AbsoluteValueFn e' uma instancia de Numero Real |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4761-4761 | AbsoluteValueFn e' uma instancia de Relacao Total |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4760-4760 | AbsoluteValueFn e' uma instancia de funcao Unaria |
No TPTP formula. May not be expressible in strict first order. | engineering.kif 134-134 | |
No TPTP formula. May not be expressible in strict first order. | engineering.kif 135-135 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4763-4763 | O contra-dominio de AbsoluteValueFn e' uma instancia de Numero Real nao-negativo |
appearance as argument number 2 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 688-688 | |
No TPTP formula. May not be expressible in strict first order. | english_format.kif 690-690 | |
No TPTP formula. May not be expressible in strict first order. | french_format.kif 417-417 | |
No TPTP formula. May not be expressible in strict first order. | relations-it.txt 18-18 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2134-2134 | |
No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 369-369 | |
No TPTP formula. May not be expressible in strict first order. | relations-de.txt 895-895 | |
No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 63-63 | |
No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 439-439 | |
No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 461-461 | |
No TPTP formula. May not be expressible in strict first order. | relations-cb.txt 52-52 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 5154-5154 | |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 689-689 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 5153-5153 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 5152-5152 | |
No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 53-53 |
antecedent |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4768-4779 | O valor absoluto de Numero Real e' igual a Numero Real nao-negativo Numero Real e' uma instancia de Numero Real Numero Real nao-negativo e' uma instancia de Numero Real Numero Real e' uma instancia de Numero Real nao-negativo Numero Real e' igual a Numero Real nao-negativo Numero Real e' uma instancia de Numero Real negativo Numero Real nao-negativo e' igual a (0.0 + Numero Real) |