SUMO   View all facts   Glossary   Help

Entity > Abstract > Class > Relation > Predicate > SententialOperator

SententialOperator comparison table

Subject	have domain2	documentation	have axiom
<=>	Formula	The truth-functional connective of bi-implication	(forall (?INT) (domain exhaustiveDecomposition ?INT Class))
=>	Formula	The truth-functional connective of implication	(forall (?INT) (domain exhaustiveDecomposition ?INT Class))
and	Formula	The truth-functional connective of conjunction	(forall (?INT) (domain exhaustiveDecomposition ?INT Class))
entails	Formula	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	(=> (and (holdsDuring ?TIME ?SITUATION1) (entails ?SITUATION1 ?SITUATION2)) (holdsDuring ?TIME ?SITUATION2))
not		The truth-functional connective of negation	(forall (?INT) (domain exhaustiveDecomposition ?INT Class))
or	Formula	The truth-functional connective of disjunction	(forall (?INT) (domain exhaustiveDecomposition ?INT Class))

Next Predicate: TernaryPredicate    Up: Predicate    Previous Predicate: QuintaryPredicate