| appearance as argument number 1 |
|
| s__documentation(s__entails__m,s__ChineseLanguage,'"这是逻辑蕴涵的运算符。(entails ?FORMULA1 ?FORMULA2) 的意思是 ?FORMULA2 可以通过SUO-KIF的证明理论从 ?FORMULA1 得出来。"')
|
chinese_format.kif 1543-1544 | |
| s__documentation(s__entails__m,s__EnglishLanguage,'"The operator of logical entailment. (entails ?FORMULA1 ?FORMULA2) means that ?FORMULA2 can be derived from ?FORMULA1 by means of the proof theory of SUO-KIF."')
|
Merge.kif 738-740 | |
| s__domain(s__entails__m,n__1,s__Formula)
|
Merge.kif 735-735 | The number 1 argument of entails is an instance of formula |
| s__domain(s__entails__m,n__2,s__Formula)
|
Merge.kif 736-736 | The number 2 argument of entails is an instance of formula |
| s__instance(s__BinaryPredicate,s__SetOrClass) s__instance(s__entails__m,s__BinaryPredicate)
|
Merge.kif 734-734 | entails is an instance of binary predicate |
| appearance as argument number 2 |
|
|
| s__format(s__ChineseLanguage,s__entails__m,'"%1 %n{doesnt} entails %2"')
|
chinese_format.kif 295-295 | |
| s__format(s__EnglishLanguage,s__entails__m,'"%1 %n{doesnt} entail%p{s} %2"')
|
english_format.kif 303-303 | |
| s__termFormat(s__ChineseLanguage,s__entails__m,'"意味"')
|
domainEnglishFormat.kif 22111-22111 | |
| s__termFormat(s__ChineseLanguage,s__entails__m,'"蕴涵"')
|
chinese_format.kif 296-296 | |
| s__termFormat(s__ChineseTraditionalLanguage,s__entails__m,'"意味"')
|
domainEnglishFormat.kif 22110-22110 | |
| s__termFormat(s__EnglishLanguage,s__entails__m,'"entails"')
|
domainEnglishFormat.kif 22109-22109 |
| antecedent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3717-3721 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16076-16080 |
|
| consequent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 27682-27694 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 15636-15645 |
|
|
Show full definition with tree view
Show simplified definition (without tree view)
Show simplified definition (with tree view)
|
|
Sigma web home Suggested Upper Merged Ontology (SUMO) web home
Sigma version 2.99c (>= 2017/11/20) is open source software produced by Articulate Software and its partners