SUMO   View all facts   Glossary   Help
Entity > Abstract > Class > Relation > BinaryRelation > BinaryPredicate > finishes
Next BinaryPredicate: frequency    Up: BinaryPredicate, IrreflexiveRelation, TemporalRelation, TransitiveRelation    Previous BinaryPredicate: fills   

finishes
subjectfact 
finishesdocumentation (finishes ?INTERVAL1 ?INTERVAL2) means that ?INTERVAL1 and ?INTERVAL2 are both TimeIntervals that have the same ending TimePoint and that ?INTERVAL2 begins before ?INTERVAL12001-11-30 13:34:16.0
has domain1 TimeInterval2001-11-30 13:34:16.0
has domain2 TimeInterval2001-11-30 13:34:16.0
is an instance of BinaryPredicate2001-11-30 13:34:16.0
is an instance of IrreflexiveRelation2001-11-30 13:34:16.0
is an instance of TemporalRelation2001-11-30 13:34:16.0
is an instance of TransitiveRelation2001-11-30 13:34:16.0
BinaryPredicatehas axiom 
(=>
 	(instance ?REL BinaryPredicate)
 	(valence ?REL 2))
2001-11-30 13:33:44.0
IrreflexiveRelationhas axiom 
(=>
    (instance ?REL IrreflexiveRelation)
    (forall (?INST)
       (not 
          (holds ?REL ?INST ?INST))))
2001-11-30 13:34:32.0
TransitiveRelationhas axiom 
(=> 
    (partialOrderingOn ?RELATION ?CLASS)
    (and 
       (reflexiveOn ?RELATION ?CLASS)
       (instance ?RELATION TransitiveRelation)
       (instance ?RELATION AntisymmetricRelation)))
2001-11-30 13:35:28.0
has axiom 
(=>
    (equivalenceRelationOn ?RELATION ?CLASS)
    (and
       (instance ?RELATION TransitiveRelation)
       (instance ?RELATION SymmetricRelation)
       (reflexiveOn ?RELATION ?CLASS)))
2001-11-30 13:35:28.0
has axiom 
(=>
    (instance ?REL TransitiveRelation)
    (forall (?INST1 ?INST2 ?INST3)
       (=>
          (and
             (holds ?REL ?INST1 ?INST2)
             (holds ?REL ?INST2 ?INST3))
          (holds ?REL ?INST1 ?INST3))))
2001-11-30 13:35:28.0
BinaryRelationis first domain of DomainFn2001-11-30 13:33:44.0
is first domain of equivalenceRelationOn2001-11-30 13:33:44.0
is first domain of inverse2001-11-30 13:33:44.0
is first domain of irreflexiveOn2001-11-30 13:33:44.0
is first domain of partialOrderingOn2001-11-30 13:33:44.0
is first domain of RangeFn2001-11-30 13:33:44.0
is first domain of reflexiveOn2001-11-30 13:33:44.0
is first domain of totalOrderingOn2001-11-30 13:33:44.0
is first domain of trichotomizingOn2001-11-30 13:33:44.0
is second domain of inverse2001-11-30 13:33:44.0
Predicateis first domain of singleValued2001-11-30 13:35:02.0
Relationis first domain of domain2001-11-30 13:35:10.0
is first domain of domainSubclass2001-11-30 13:35:10.0
is first domain of holds2001-11-30 13:35:10.0
is first domain of subrelation2001-11-30 13:35:10.0
is first domain of valence2001-11-30 13:35:10.0
is second domain of subrelation2001-11-30 13:35:10.0
Classis third domain of domain2001-11-30 13:33:51.0
is third domain of domainSubclass2001-11-30 13:33:51.0
Abstractis disjoint from Physical2001-11-30 13:33:32.0

Next BinaryPredicate: frequency    Up: BinaryPredicate, IrreflexiveRelation, TemporalRelation, TransitiveRelation    Previous BinaryPredicate: fills