SUMO   View all facts   Glossary   Help
Entity > Abstract > Class > Relation > Function > BinaryFunction > KappaFn
Next BinaryFunction: LogFn    Up: BinaryFunction    Previous BinaryFunction: IntersectionFn   

KappaFn
subjectfact 
KappaFndocumentation A class-forming operator that takes two arguments: a variable and a formula containing at least one unbound occurrence of the variable. The result of applying KappaFn to a variable and a formula is the Class of things that satisfy the formula. For example, we can denote the Class of prime numbers that are less than 100 with the following expression: (KappaFn ?NUMBER (and (instance ?NUMBER PrimeNumber) (lessThan ?NUMBER 100))). Note that the use of this function is discouraged, since there is currently no axiomatic support for it2001-11-30 13:34:33.0
has domain1 SymbolicString2001-11-30 13:34:33.0
has domain2 Formula2001-11-30 13:34:33.0
has range Class2001-11-30 13:34:33.0
is an instance of BinaryFunction2001-11-30 13:34:33.0
BinaryFunctionhas axiom 
(<=>
    (and
       (holds ?REL ?INST1 ?INST2 ?INST3)
       (instance ?REL BinaryFunction))
    (equal (AssignmentFn ?REL ?INST1 ?INST2) ?INST3))
2001-11-30 13:33:43.0
has axiom 
(=>
    (and
       (closedOn ?FUNCTION ?CLASS)
       (instance ?FUNCTION BinaryFunction))
    (forall (?INST1 ?INST2)
       (=> 
          (and 
             (instance ?INST1 ?CLASS) 
             (instance ?INST2 ?CLASS))
          (instance (AssignmentFn ?FUNCTION ?INST1 ?INST2) ?CLASS))))
2001-11-30 13:33:43.0
has axiom 
(=>
    (and
       (instance ?FUNCTION BinaryFunction)
       (equal (AssignmentFn ?FUNCTION ?ARG1 ?ARG2) ?VALUE1)
       (equal (AssignmentFn ?FUNCTION ?ARG1 ?ARG2) ?VALUE2))
    (equal ?VALUE1 ?VALUE2))
2001-11-30 13:33:43.0
has axiom 
(=>
    (and
       (instance ?FUNCTION RelationExtendedToQuantities)
       (instance ?FUNCTION BinaryFunction)
       (instance ?NUMBER1 RealNumber)
       (instance ?NUMBER2 RealNumber)
       (equal (AssignmentFn ?FUNCTION ?NUMBER1 ?NUMBER2) ?VALUE))
    (forall (?UNIT)
       (=>
          (instance ?UNIT UnitOfMeasure)
          (equal (AssignmentFn ?FUNCTION 
                    (MeasureFn ?NUMBER1 ?UNIT) 
                    (MeasureFn ?NUMBER2 ?UNIT)) 
                 (MeasureFn ?VALUE ?UNIT)))))
2001-11-30 13:33:43.0
has axiom 
(=>
 	(instance ?FUNCTION BinaryFunction)
 	(valence ?FUNCTION 2))
2001-11-30 13:33:43.0
is first domain of distributes2001-11-30 13:33:43.0
is first domain of identityElement2001-11-30 13:33:43.0
is second domain of distributes2001-11-30 13:33:43.0
Classis third domain of domain2001-11-30 13:33:51.0
is third domain of domainSubclass2001-11-30 13:33:51.0
Abstractis disjoint from Physical2001-11-30 13:33:32.0

Next BinaryFunction: LogFn    Up: BinaryFunction    Previous BinaryFunction: IntersectionFn