Select language: english | cesky | deutsch | italiano | simplified chinese | traditional chinese | hindi Concept: English word: Home

# 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))```