TreeView Knowledge Base Browser

appearance as argument number 1

(instance entails BinaryPredicate)	Merge.kif 761-761	entails is an instance of binary predicate
(domain entails 1 Formula)	Merge.kif 762-762	The number 1 argument of entails is an instance of formula
(domain entails 2 Formula)	Merge.kif 763-763	The number 2 argument of entails is an instance of formula
(documentation entails 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 765-767	The number 2 argument of entails is an instance of formula

appearance as argument number 2

(termFormat EnglishLanguage entails "entails")	domainEnglishFormat.kif 22181-22181
(termFormat ChineseTraditionalLanguage entails "意味")	domainEnglishFormat.kif 22182-22182
(termFormat ChineseLanguage entails "意味")	domainEnglishFormat.kif 22183-22183
(format EnglishLanguage entails "%1 %n{doesn't} entail%p{s} %2")	english_format.kif 300-300

antecedent

(=>
    (and
        (holdsDuring ?TIME ?SITUATION1)
        (entails ?SITUATION1 ?SITUATION2))
    (holdsDuring ?TIME ?SITUATION2))

Merge.kif 3991-3995

If X holds during Y and X entails Z, then Z holds during Y

consequent

(=>
    (and
        (attribute ?C Collectible)
        (hasPurpose ?C ?P))
    (exists (?H ?P2)
        (and
            (instance ?H Human)
            (wants ?H ?C)
            (desires ?H ?P2)
            (entails ?P2
                (possesses ?H ?C))
            (not
                (equal ?P ?P2)))))

Mid-level-ontology.kif 32118-32130

If Collectible is an attribute of X and X has the purpose Y, then All of the following hold: (1) there exist Z (2) W such that Z is an instance of human (3) Z wants X (4) Z desires W (5) W entails Z possesses X (6) equal Y (7) W

statement

(exists (?FORMULA1 ?FORMULA2)
    (and
        (instance ?FORMULA1 Formula)
        (containsFormula ImmigrationAndNationalityAct_US ?FORMULA1)
        (instance ?FORMULA2 Formula)
        (containsFormula ImmigrationAndNationalityAct_Section219_US ?FORMULA2)
        (entails ?FORMULA1 ?FORMULA2)))

Government.kif 2385-2391

There exist X, Y such that X is an instance of formula, immigration and nationality act_US contains the formula X, Y is an instance of formula, immigration and nationality act- section219-US contains the formula Y, and X entails Y

Show simplified definition (without tree view)
Show simplified definition (with tree view)

KB Term:			Term intersection

English Word: