tui1 zhi1 (entails)

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.

Ontology

SUMO / STRUCTURAL-ONTOLOGY

Class(es)

luo2 ji2 yun4 suan4 yuan2

tui1 zhi1

Coordinate term(s)

ruo4 qie3 wei2 ruo4 ruo4 he2 cun2 zai4 suo3 you3 fei1 huo4

Type restrictions

entails(SUO-KIFbiao3 shu4 shi4, SUO-KIFbiao3 shu4 shi4)

Related WordNet synsets

proof: (logic or mathematics) a formal series of statements showing that if one thing is true something else necessarily follows from it
entail, imply, mean: have as a logical consequence; "The water shortage means that we have to stop taking long showers"
follow: come as a logical consequence; follow logically; "It follows that your assertion is false"

See more related synsets on a separate page.

Axioms (2)

If situation1 (mei2) wei2 zhen1 timea(zhi1 zhong1) time and tui1 zhi1(situation1,situation2) holds, then situation2 (mei2) wei2 zhen1 timea(zhi1 zhong1) time.

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

If chen2 shu4 formula1 you3 prop de5 xing2 tai4 yi4 yi4 and tui1 zhi1(formula1,formula2) holds, then chen2 shu4 formula2 you3 prop de5 xing2 tai4 yi4 yi4.

(=>
      (and
            (modalAttribute ?FORMULA1 ?PROP)
            (entails ?FORMULA1 ?FORMULA2))
      (modalAttribute ?FORMULA2 ?PROP))