entails (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)

logical operator

entails

Coordinate term(s)

<=> => and exists forall not or

Type restrictions

entails(formula, formula)

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 holds during time and situation1 entails situation2, then situation2 holds during time.

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

If the statement formula1 has the model force of prop and formula1 entails formula2, then the statement formula2 has the model force of prop.

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