SUMO   View all facts   Glossary   Help
Entity > Abstract > Class > Relation > BinaryRelation > BinaryPredicate > distributes
Next BinaryPredicatedocumentation    UpBinaryPredicate, BinaryRelation    Previous BinaryPredicatedisjoint   

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))
BinaryRelation  trichotomizingOnBinaryRelations map instances of a Class to instances of another Class. BinaryRelations are represented as slots in frame systems
(inverse ?REL1 ?REL2)
(instance ?REL1 BinaryRelation)
(instance ?REL2 BinaryRelation))
(forall (?INST1 ?INST2)
(holds ?REL1 ?INST1 ?INST2)
(holds ?REL2 ?INST2 ?INST1))))
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)
(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))))))

Next BinaryPredicatedocumentation    UpBinaryPredicate, BinaryRelation    Previous BinaryPredicatedisjoint