SUMO   View all facts   Glossary   Help
Entity > Abstract > Class > Relation > BinaryRelation > BinaryPredicate > finishes
Next BinaryPredicatefrequency    UpBinaryPredicate, IrreflexiveRelation, TemporalRelation, TransitiveRelation    Previous BinaryPredicatefills   

finishes comparison table
Subject have domain2 have domain1 be first domain of be second domain of documentation have axiom is a kind of is an instance of
BinaryPredicate  singleValuedinverseA Predicate relating two items - its valence is two
(=>
(instance ?REL BinaryPredicate)
(valence ?REL 2))
Predicate 
IrreflexiveRelation  trichotomizingOninverseRelation ?REL is irreflexive if (?REL ?INST ?INST) holds for no value of ?INST
(=>
(instance ?REL IrreflexiveRelation)
(forall (?INST)
(not
(holds ?REL ?INST ?INST))))
BinaryRelation 
TemporalRelation  valencesubrelationThe Class of temporal Relations. This Class includes notions of (temporal) topology of intervals, (temporal) schemata, and (temporal) extension
(forall (?INT) (domain exhaustiveDecomposition ?INT Class))
Relation 
TransitiveRelation  trichotomizingOninverseA BinaryRelation ?REL is transitive if (?REL ?INST1 ?INST2) and (?REL ?INST2 ?INST3) imply (?REL ?INST1 ?INST3), for all ?INST1, ?INST2, and ?INST3
(=>
(instance ?REL TransitiveRelation)
(forall (?INST1 ?INST2 ?INST3)
(=>
(and
(holds ?REL ?INST1 ?INST2)
(holds ?REL ?INST2 ?INST3))
(holds ?REL ?INST1 ?INST3))))
BinaryRelation 
finishesTimeIntervalTimeIntervalvalencesubrelation(finishes ?INTERVAL1 ?INTERVAL2) means that ?INTERVAL1 and ?INTERVAL2 are both TimeIntervals that have the same ending TimePoint and that ?INTERVAL2 begins before ?INTERVAL1
(=>
(instance ?REL TransitiveRelation)
(forall (?INST1 ?INST2 ?INST3)
(=>
(and
(holds ?REL ?INST1 ?INST2)
(holds ?REL ?INST2 ?INST3))
(holds ?REL ?INST1 ?INST3))))
 TransitiveRelation

Next BinaryPredicatefrequency    UpBinaryPredicate, IrreflexiveRelation, TemporalRelation, TransitiveRelation    Previous BinaryPredicatefills