Browsing Interface : Welcome guest : log in
|
Browsing Interface : Welcome guest : log in |
[
Home |
Graph |
LogLearn |
Editor |
]
KB:
Language:
Formal Language:
|
| AssignmentFn |
| appearance as argument number 1 |
|
| (instance AssignmentFn Function) | Merge.kif 776-776 | Assignment is an instance of function |
| (instance AssignmentFn VariableArityRelation) | Merge.kif 777-777 | Assignment is an instance of variable arity relation |
| (domain AssignmentFn 1 Function) | Merge.kif 778-778 | The number 1 argument of assignment is an instance of function |
| (domain AssignmentFn 2 Entity) | Merge.kif 779-779 | The number 2 argument of assignment is an instance of entity |
| (range AssignmentFn Entity) | Merge.kif 780-780 | The range of assignment is an instance of entity |
| (documentation AssignmentFn EnglishLanguage "If F is a Function with a value for the objects denoted by N1,..., NK, then (AssignmentFn F N1 ... NK) is the value of applying F to the objects denoted by N1,..., NK. Otherwise, the value is undefined.") | Merge.kif 782-785 | The range of assignment is an instance of entity |
| appearance as argument number 2 |
|
|
| antecedent |
|
|
| (=> (and (range ?FUNCTION ?CLASS) (equal (AssignmentFn ?FUNCTION @ROW) ?VALUE)) (instance ?VALUE ?CLASS)) |
Merge.kif 305-309 | If the range of X is an instance of Y and equal X(@ROW) and W, then W is an instance of Y |
| (=> (and (rangeSubclass ?FUNCTION ?CLASS) (equal (AssignmentFn ?FUNCTION @ROW) ?VALUE)) (subclass ?VALUE ?CLASS)) |
Merge.kif 331-335 | If the values returned by X are subclasses of Y and equal X(@ROW) and W, then W is a subclass of Y |
| consequent |
|
|
| (=> (instance ?FUN OneToOneFunction) (forall (?ARG1 ?ARG2) (=> (exists (?CLASS) (and (domain ?FUN 1 ?CLASS) (instance ?ARG1 ?CLASS) (instance ?ARG2 ?CLASS) (not (equal ?ARG1 ?ARG2)))) (not (equal (AssignmentFn ?FUN ?ARG1) (AssignmentFn ?FUN ?ARG2)))))) |
Merge.kif 3488-3498 | If X is an instance of one to one function, then For all Entities Y and Z: if there exists W such that the number 1 argument of X is an instance of W, Y is an instance of W, Z is an instance of W, equal Y, and Z, then equal X(Y) and X(Z) |
| (=> (instance ?FUNCTION AssociativeFunction) (forall (?INST1 ?INST2 ?INST3 ?CLASS) (=> (and (domain ?FUNCTION 1 ?CLASS) (instance ?INST1 ?CLASS) (instance ?INST2 ?CLASS) (instance ?INST3 ?CLASS)) (equal (AssignmentFn ?FUNCTION ?INST1 (AssignmentFn ?FUNCTION ?INST2 ?INST3)) (AssignmentFn ?FUNCTION (AssignmentFn ?FUNCTION ?INST1 ?INST2) ?INST3))))) |
Merge.kif 3531-3541 | If X is an instance of associative function, then For all Entities Y, Z, and W and Class V: if the number 1 argument of X is an instance of V, Y is an instance of V, Z is an instance of V, and W is an instance of V, then equal X(Y and X(Z and W)) and X(X(Y and Z) and W) |
| (=> (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) |
|