![]() |
![]() Browsing Interface : Welcome guest : log in |
[
Home | 
Graph | 
LogLearn |
Editor |
]
KB:
Language:
Formal Language:
|
| CommutativeFunction(commutative function) | commutative |
| appearance as argument number 1 |
|
|
| (subclass CommutativeFunction BinaryFunction) | Merge.kif 3543-3543 | Commutative function is a subclass of binary function |
| (documentation CommutativeFunction EnglishLanguage "A BinaryFunction is commutative if the ordering of the arguments of the function has no effect on the value returned by the function. More precisely, a function ?FUNCTION is commutative just in case (?FUNCTION ?INST1 ?INST2) is equal to (?FUNCTION ?INST2 ?INST1), for all ?INST1 and ?INST2.") | Merge.kif 3545-3549 | Commutative function is a subclass of binary function |
| (externalImage CommutativeFunction "http://upload.wikimedia.org/wikipedia/ commons/ d/ da/ Commutative_Word_Origin.PNG") | pictureList.kif 8429-8429 | Commutative function is a subclass of binary function |
| appearance as argument number 2 |
|
|
| antecedent |
|
|
| (=> (instance ?FUNCTION CommutativeFunction) (forall (?INST1 ?INST2 ?CLASS) (=> (and (domain ?FUNCTION 1 ?CLASS) (instance ?INST1 ?CLASS) (instance ?INST2 ?CLASS)) (equal (AssignmentFn ?FUNCTION ?INST1 ?INST2) (AssignmentFn ?FUNCTION ?INST2 ?INST1))))) |
Merge.kif 3551-3561 | If X is an instance of commutative function, then For all Entities Y and Z and Class W: if the number 1 argument of X is an instance of W, Y is an instance of W, and Z is an instance of W, then equal X(Y and Z) and X(Z and Y) |