SUMO   View all facts   Glossary   Help
Entity > Abstract > Class > Relation > BinaryRelation > BinaryPredicate > distributes
Next BinaryPredicate: documentation    Up: BinaryPredicate, BinaryRelation    Previous BinaryPredicate: disjoint   

distributes comparison table
Subject have domain2 have domain1 be first domain of documentation have axiom is a kind of is an instance of
BinaryPredicate  singleValuedA Predicate relating two items - its valence is two
(=>
 	(instance ?REL BinaryPredicate)
 	(valence ?REL 2))
Predicate 
BinaryRelation  trichotomizingOnBinaryRelations map instances of a Class to instances of another Class. BinaryRelations are represented as slots in frame systems
(=>
    (and
       (inverse ?REL1 ?REL2)
       (instance ?REL1 BinaryRelation)
       (instance ?REL2 BinaryRelation))
    (forall (?INST1 ?INST2)
       (<=>
          (holds ?REL1 ?INST1 ?INST2)
          (holds ?REL2 ?INST2 ?INST1))))
Relation 
distributesBinaryFunctionBinaryFunctiontrichotomizingOnA BinaryFunction ?FUNCTION1 is distributive over another BinaryFunction ?FUNCTION2 just in case (?FUNCTION1 ?INST1 (?FUNCTION2 ?INST2 ?INST3)) is equal to (?FUNCTION2 (?FUNCTION1 ?INST1 ?INST2) (?FUNCTION1 ?INST1 ?INST3)), for all ?INST1, ?INST2, and ?INST3
(=>
    (distributes ?FUNCTION1 ?FUNCTION2)
    (forall (?INST1 ?INST2 ?INST3)
       (=>
          (and
             (instance ?INST1 (DomainFn ?FUNCTION1))
             (instance ?INST2 (DomainFn ?FUNCTION1))
             (instance ?INST3 (DomainFn ?FUNCTION1))
             (instance ?INST1 (DomainFn ?FUNCTION2))
             (instance ?INST2 (DomainFn ?FUNCTION2))
             (instance ?INST3 (DomainFn ?FUNCTION2)))
          (equal (AssignmentFn ?FUNCTION1 ?INST1 
                         (AssignmentFn ?FUNCTION2 ?INST2 ?INST3))
                 (AssignmentFn ?FUNCTION2 
                         (AssignmentFn ?FUNCTION1 ?INST1 ?INST2) 
                         (AssignmentFn ?FUNCTION1 ?INST1 ?INST3))))))
 BinaryRelation

Next BinaryPredicate: documentation    Up: BinaryPredicate, BinaryRelation    Previous BinaryPredicate: disjoint