| Subject |
have domain2 |
have domain1 |
be first domain of |
documentation |
have axiom |
is a kind of |
is an instance of |
|---|
| AntisymmetricRelation | | | trichotomizingOn | BinaryRelation ?REL is an AntisymmetricRelation if for distinct ?INST1 and ?INST2, (?REL ?INST1 ?INST2) implies not (?REL ?INST2 ?INST1). In other words, for all ?INST1 and ?INST2, (?REL ?INST1 ?INST2) and (?REL ?INST2 ?INST1) imply that ?INST1 and ?INST2 are identical. Note that it is possible for an AntisymmetricRelation to be a ReflexiveRelation | (=>
(instance ?REL AntisymmetricRelation)
(forall (?INST1 ?INST2)
(=>
(and
(holds ?REL ?INST1 ?INST2)
(holds ?REL ?INST2 ?INST1))
(equal ?INST1 ?INST2))))
| BinaryRelation | |
| BinaryPredicate | | | singleValued | A Predicate relating two items - its valence is two | (=>
(instance ?REL BinaryPredicate)
(valence ?REL 2))
| Predicate | |
| distributes | BinaryFunction | BinaryFunction | trichotomizingOn | A 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 |
| IntransitiveRelation | | | trichotomizingOn | A BinaryRelation ?REL is intransitive only if (?REL ?INST1 ?INST2) and (?REL ?INST2 ?INST3) imply not (?REL ?INST1 ?INST3), for all ?INST1, ?INST2, and ?INST3 | (=>
(instance ?REL IntransitiveRelation)
(forall (?INST1 ?INST2 ?INST3)
(=>
(and
(holds ?REL ?INST1 ?INST2)
(holds ?REL ?INST2 ?INST3))
(not
(holds ?REL ?INST1 ?INST3)))))
| BinaryRelation | |
| IrreflexiveRelation | | | trichotomizingOn | Relation ?REL is irreflexive if (?REL ?INST ?INST) holds for no value of ?INST | (=>
(instance ?REL IrreflexiveRelation)
(forall (?INST)
(not
(holds ?REL ?INST ?INST))))
| BinaryRelation | |
| ReflexiveRelation | | | trichotomizingOn | Relation ?REL is reflexive if (?REL ?INST ?INST) for all ?INST | (=>
(instance ?REL ReflexiveRelation)
(forall (?INST)
(holds ?REL ?INST ?INST)))
| BinaryRelation | |
| SymmetricRelation | | | trichotomizingOn | A BinaryRelation ?REL is symmetric just in case (?REL ?INST1 ?INST2) imples (?REL ?INST2 ?INST1), for all ?INST1 and ?INST2 | (=>
(instance ?REL SymmetricRelation)
(forall (?INST1 ?INST2)
(=>
(holds ?REL ?INST1 ?INST2)
(holds ?REL ?INST2 ?INST2))))
| BinaryRelation | |
| TransitiveRelation | | | trichotomizingOn | A 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 | |
| TrichotomizingRelation | | | trichotomizingOn | A BinaryRelation ?REL is a TrichotomizingRelation just in case all ordered pairs consisting of distinct individuals are elements of ?REL | (=>
(instance ?REL TrichotomizingRelation)
(forall (?INST1 ?INST2)
(or
(holds ?REL ?INST1 ?INST2)
(equal ?INST1 ?INST2)
(holds ?REL ?INST2 ?INST1))))
| BinaryRelation | |
| UnaryFunction | | | rangeSubclass | The Class of Functions that require a single argument | (=>
(instance ?FUNCTION UnaryFunction)
(valence ?FUNCTION 1))
| Function | |
SUMO View all facts Glossary Help
