Browsing Interface : Welcome guest : log in
Home |  Graph |  ]  KB:  Language:   

Formal Language: 



KB Term:  Term intersection
English Word: 

Sigma KEE - entails
entails

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