Subject |
have domain2 |
have domain1 |
partition into |
be first domain of |
have range |
documentation |
have inverse |
have axiom |
is a kind of |
is an instance of |
AbsoluteValueFn | | RealNumber | | rangeSubclass | PositiveRealNumber | The value of (AbsoluteValueFn ?NUMBER) is the absolute value of the RealNumber ?NUMBER | | (<=> (equal (AbsoluteValueFn ?NUMBER1) ?NUMBER2) (or (and (instance ?NUMBER1 PositiveInteger) (equal ?NUMBER1 ?NUMBER2)) (and (instance ?NUMBER1 NegativeInteger) (equal ?NUMBER2 (SubtractionFn 0 ?NUMBER1)))))
| | UnaryFunction |
AbstractionFn | | Class | | rangeSubclass | Attribute | A UnaryFunction that maps a Class into the instance of Attribute that specifies the condition(s) for membership in the Class | | (<=> (equal (AbstractionFn ?CLASS) ?ATTR) (forall (?INST) (<=> (instance ?INST ?CLASS) (attribute ?INST ?ATTR))))
| | UnaryFunction |
ArcCosineFn | | RealNumber | | rangeSubclass | PlaneAngleMeasure | (ArcCosineFn ?NUMBER) returns the arc cosine of the RealNumber ?NUMBER. It is the inverse of CosineFn | CosineFn | (=> (instance ?FUNCTION UnaryFunction) (valence ?FUNCTION 1))
| | UnaryFunction |
ArcSineFn | | RealNumber | | rangeSubclass | PlaneAngleMeasure | (ArcSineFn ?NUMBER) returns the arc sine of the RealNumber ?NUMBER. It is the inverse of SineFn | SineFn | (=> (instance ?FUNCTION UnaryFunction) (valence ?FUNCTION 1))
| | UnaryFunction |
ArcTangentFn | | RealNumber | | rangeSubclass | PlaneAngleMeasure | (ArcTangentFn ?NUMBER) returns the arc tangent of the RealNumber ?NUMBER. It is the inverse of TangentFn | TangentFn | (=> (instance ?FUNCTION UnaryFunction) (valence ?FUNCTION 1))
| | UnaryFunction |
BeginFn | | TimeInterval | | rangeSubclass | TimePoint | A UnaryFunction that maps a TimeInterval to the TimePoint at which the interval begins | | (equal (BeginFn (PastFn ?TIME)) NegativeInfinity)
| | UnaryFunction |
CardinalityFn | NonnegativeInteger | (UnionFn Class Collection) | | rangeSubclass | | (CardinalityFn ?CLASS) returns the number of instances in the Class or Collection ?CLASS | | (=> (instance ?SET FiniteSet) (exists (?NUMBER) (and (instance ?NUMBER NonnegativeInteger) (equal ?NUMBER (CardinalityFn ?SET)))))
| | UnaryFunction |
CeilingFn | | RealNumber | | rangeSubclass | Integer | (CeilingFn ?NUMBER) returns the smallest Integer greater than or equal to the RealNumber ?NUMBER | | (=> (equal (RoundFn ?NUMBER1) ?NUMBER2) (or (=> (lessThan (SubtractionFn ?NUMBER1 (FloorFn ?NUMBER1)) .5) (equal ?NUMBER2 (FloorFn ?NUMBER1))) (=> (greaterThanOrEqualTo (SubtractionFn ?NUMBER1 (FloorFn ?NUMBER1)) .5) (equal ?NUMBER2 (CeilingFn ?NUMBER1)))))
| | UnaryFunction |
ComplementFn | | Class | | rangeSubclass | Class | The complement of a given Class C is the Class of all things that are not instances of C. In other words, an object is an instance of the complement of a Class C just in case it is not an instance of C | | (equal NullSet (ComplementFn Entity))
| | UnaryFunction |
CosineFn | | PlaneAngleMeasure | | rangeSubclass | RealNumber | (CosineFn ?DEGREE) returns the cosine of the PlaneAngleMeasure ?DEGREE. The cosine of ?DEGREE is the ratio of the side next to ?DEGREE to the hypotenuse in a right-angled triangle | | (equal (TangentFn ?DEGREE) (DivisionFn (SineFn ?DEGREE) (CosineFn ?DEGREE)))
| | UnaryFunction |
DenominatorFn | | RealNumber | | rangeSubclass | Integer | (DenominatorFn ?NUMBER) returns the denominator of the canonical reduced form of the RealNumber ?NUMBER | | (=> (instance ?FUNCTION UnaryFunction) (valence ?FUNCTION 1))
| | UnaryFunction |
DomainFn | | BinaryRelation | | rangeSubclass | Class | The domain of a BinaryRelation ?REL is the Class of all things that bear ?REL to something | | (=> (instance ?FUNCTION CommutativeFunction) (forall (?INST1 ?INST2) (=> (and (instance ?INST1 (DomainFn ?FUNCTION)) (instance ?INST2 (DomainFn ?FUNCTION))) (equal (AssignmentFn ?FUNCTION ?INST1 ?INST2) (AssignmentFn ?FUNCTION ?INST2 ?INST1)))))
| | UnaryFunction |
EndFn | | TimeInterval | | rangeSubclass | TimePoint | A UnaryFunction that maps a TimeInterval to the TimePoint at which the interval ends | | (equal (EndFn (FutureFn ?TIME)) PositiveInfinity)
| | UnaryFunction |
EngineeringComponentFn | | Terminal | | rangeSubclass | EngineeringComponent | A UnaryFunction that maps a Terminal to its corresponding EngineeringComponent | TerminalFn | (=> (instance ?FUNCTION UnaryFunction) (valence ?FUNCTION 1))
| | UnaryFunction |
ExtensionFn | | Attribute | | rangeSubclass | Class | A UnaryFunction that maps an Attribute into the Class whose condition for membership is the Attribute | | (<=> (equal (ExtensionFn ?ATTRIBUTE) ?CLASS) (equal (AttributeFn ?CLASS) ?ATTRIBUTE))
| | UnaryFunction |
FloorFn | | RealNumber | | rangeSubclass | Integer | (FloorFn ?NUMBER) returns the largest Integer less than or equal to the RealNumber ?NUMBER | | (=> (equal (RoundFn ?NUMBER1) ?NUMBER2) (or (=> (lessThan (SubtractionFn ?NUMBER1 (FloorFn ?NUMBER1)) .5) (equal ?NUMBER2 (FloorFn ?NUMBER1))) (=> (greaterThanOrEqualTo (SubtractionFn ?NUMBER1 (FloorFn ?NUMBER1)) .5) (equal ?NUMBER2 (CeilingFn ?NUMBER1)))))
| | UnaryFunction |
FutureFn | | TimePosition | | rangeSubclass | TimeInterval | A UnaryFunction that maps a TimePosition to the TimeInterval which it meets and which ends at PositiveInfinity | | (starts (ImmediateFutureFn (WhenFn ?THING)) (FutureFn (WhenFn ?THING)))
| | UnaryFunction |
GeneralizedIntersectionFn | | Class | | rangeSubclass | Class | A UnaryFunction that takes a Class of Classes as its single argument and returns a Class which is the intersection of all of the Classes in the original Class, i.e. the Class containing just those instances which are instances of all instances of the original Class | | (=> (instance ?CLASS MutuallyDisjointClass) (equal (GeneralizedIntersectionFn ?CLASS) NullSet))
| | UnaryFunction |
GeneralizedUnionFn | | Class | | rangeSubclass | Class | A UnaryFunction that takes a Class of Classes as its single argument and returns a Class which is the merge of all of the Classes in the original Class, i.e. the Class containing just those instances which are instances of an instance of the original Class | | (<=> (instance ?ENTITY (GeneralizedUnionFn ?SUPERCLASS)) (exists (?CLASS) (and (instance ?CLASS ?SUPERCLASS) (instance ?ENTITY ?CLASS))))
| | UnaryFunction |
IdentityFn | | Entity | | rangeSubclass | Entity | The value of the identity function is just its argument | | (equal (IdentityFn ?INST) ?INST)
| | UnaryFunction |
ImaginaryPartFn | | ComplexNumber | | rangeSubclass | ImaginaryNumber | (ImaginaryPartFn ?NUMBER) returns the imaginary part of ?NUMBER | | (=> (instance ?NUMBER ComplexNumber) (exists (?PART1 ?PART2) (and (equal ?PART1 (RealNumberFn ?NUMBER)) (equal ?PART2 (ImaginaryPartFn ?NUMBER)))))
| | UnaryFunction |
ImmediateFutureFn | | TimePosition | | rangeSubclass | TimeInterval | A UnaryFunction that maps a TimePosition to a short, indeterminate TimeInterval that immediately follows the TimePosition | | (starts (ImmediateFutureFn (WhenFn ?THING)) (FutureFn (WhenFn ?THING)))
| | UnaryFunction |
ImmediatePastFn | | TimePosition | | rangeSubclass | TimeInterval | A UnaryFunction that maps a TimePosition to a short, indeterminate TimeInterval that immediately precedes the TimePosition | | (finishes (ImmediatePastFn (WhenFn ?THING)) (PastFn (WhenFn ?THING)))
| | UnaryFunction |
IntegerSquareRootFn | | RealNumber | | rangeSubclass | NonnegativeInteger | (IntegerSquareRootFn ?NUMBER) returns the integer square root of ?NUMBER | | (=> (instance ?FUNCTION UnaryFunction) (valence ?FUNCTION 1))
| | UnaryFunction |
JunctionFn | | Terminal | | rangeSubclass | Junction | A UnaryFunction that maps a Terminal to its corresponding Junction | | (=> (instance ?FUNCTION UnaryFunction) (valence ?FUNCTION 1))
| | UnaryFunction |
MagnitudeFn | | ConstantQuantity | | rangeSubclass | RealNumber | The magnitude of a ConstantQuantity is the numeric value for the quantity. In other words, MagnitudeFn converts a ConstantQuantity with an associated UnitOfMeasure into an ordinary RealNumber. For example, the magnitude of the ConstantQuantity 2 Kilometers is the RealNumber 2. Note that the magnitude of a quantity in a given unit times that unit is equal to the original quantity | | (equal (MagnitudeFn (MeasureFn ?NUMBER ?UNIT)) ?NUMBER)
| | UnaryFunction |
NumeratorFn | | RealNumber | | rangeSubclass | Integer | (NumeratorFn ?NUMBER) returns the numerator of the canonical reduced form ?NUMBER | | (=> (instance ?FUNCTION UnaryFunction) (valence ?FUNCTION 1))
| | UnaryFunction |
OneToOneFunction | | | | rangeSubclass | | The Class of UnaryFunctions which are one to one. A function F is one to one just in case for all X, Y in the domain of F, if X is not identical to Y, then F(X) is not identical to F(Y) | | (<=> (instance ?FUN OneToOneFunction) (forall (?ARG1 ?ARG2) (=> (and (instance ?ARG1 (DomainFn ?FUN)) (instance ?ARG2 (DomainFn ?FUN)) (not (equal ?ARG1 ?ARG2))) (not (equal (AssignmentFn ?FUN ?ARG1) (AssignmentFn ?FUN ?ARG2))))))
| UnaryFunction | |
PastFn | | TimePosition | | rangeSubclass | TimeInterval | A UnaryFunction that maps a TimePosition to the TimeInterval that meets it and that begins at NegativeInfinity | | (meetsTemporally (PastFn (WhenFn ?THING)) (WhenFn ?THING))
| | UnaryFunction |
PredecessorFn | | Integer | | rangeSubclass | Integer | A UnaryFunction that maps an Integer to its predecessor, e.g. the predecessor of 5 is 4 | | (=> (instance ?INT Integer) (greaterThan ?INT (PredecessorFn ?INT)))
| | UnaryFunction |
PrincipalHostFn | | Hole | | rangeSubclass | Object | A UnaryFunction that maps a Hole to the Object which is its principal host. The principle host of a Hole is its maximally connected host (a notion taken here to be defined only when the argument is a hole) | | (=> (equal ?OBJ1 (SkinFn ?HOLE)) (forall (?OBJ2) (<=> (overlapsSpatially ?OBJ2 ?OBJ1) (exists (?OBJ3) (and (superficialPart ?OBJ3 (PrincipalHostFn ?HOLE)) (meetsSpatially ?HOLE ?OBJ3) (overlapsSpatially ?OBJ2 ?OBJ3))))))
| | UnaryFunction |
PropertyFn | | Agent | | rangeSubclass | Set | A UnaryFunction that maps an Agent to the Set of Property owned by the Agent | | (<=> (equal (WealthFn ?PERSON) ?AMOUNT) (monetaryValue (PropertyFn ?PERSON) ?AMOUNT))
| | UnaryFunction |
RangeFn | | BinaryRelation | | rangeSubclass | Class | The range of a BinaryRelation ?REL is the Class of all things such that something bears ?REL to them | | (=> (instance ?SEQ SequenceFunction) (subclass (RangeFn ?SEQ) Integer))
| | UnaryFunction |
RationalNumberFn | | Number | | rangeSubclass | RationalNumber | (RationalNumberFn ?NUMBER) returns the rational representation of ?NUMBER | | (=> (instance ?FUNCTION UnaryFunction) (valence ?FUNCTION 1))
| | UnaryFunction |
RealNumberFn | | Number | | rangeSubclass | RealNumber | (RealNumberFn ?NUMBER) returns the part of ?NUMBER that is a RealNumber | | (=> (instance ?NUMBER ComplexNumber) (exists (?PART1 ?PART2) (and (equal ?PART1 (RealNumberFn ?NUMBER)) (equal ?PART2 (ImaginaryPartFn ?NUMBER)))))
| | UnaryFunction |
ReciprocalFn | | Quantity | | rangeSubclass | Quantity | (ReciprocalFn ?NUMBER) is the reciprocal element of ?NUMBER with respect to the multiplication operator (MultiplicationFn), i.e. 1/?NUMBER. Not all numbers have a reciprocal element. For example the number 0 does not. If a number ?NUMBER has a reciprocal ?RECIP, then the product of ?NUMBER and ?RECIP will be 1, e.g. 3*1/3 = 1. The reciprocal of an element is equal to applying the ExponentiationFn function to the element to the power -1 | | (equal 1 (MultiplicationFn ?NUMBER (ReciprocalFn ?NUMBER)))
| | UnaryFunction |
RoundFn | | Quantity | | rangeSubclass | Quantity | (RoundFn ?NUMBER) is the Integer closest to ?NUMBER on the number line. If ?NUMBER is halfway between two Integers (for example 3.5), it denotes the larger Integer | | (=> (equal (RoundFn ?NUMBER1) ?NUMBER2) (or (=> (lessThan (SubtractionFn ?NUMBER1 (FloorFn ?NUMBER1)) .5) (equal ?NUMBER2 (FloorFn ?NUMBER1))) (=> (greaterThanOrEqualTo (SubtractionFn ?NUMBER1 (FloorFn ?NUMBER1)) .5) (equal ?NUMBER2 (CeilingFn ?NUMBER1)))))
| | UnaryFunction |
SignumFn | | RealNumber | | rangeSubclass | Integer | (SignumFn ?NUMBER) denotes the sign of ?NUMBER. This is one of the following values: -1, 1, or 0 | | (=> (instance ?NUMBER PositiveRealNumber) (equal (SignumFn ?NUMBER) 1))
| | UnaryFunction |
SineFn | | PlaneAngleMeasure | | rangeSubclass | RealNumber | (SineFn ?DEGREE) is the sine of the PlaneAngleMeasure ?DEGREE. The sine of ?DEGREE is the ratio of the side opposite ?DEGREE to the hypotenuse in a right-angled triangle | | (equal (TangentFn ?DEGREE) (DivisionFn (SineFn ?DEGREE) (CosineFn ?DEGREE)))
| | UnaryFunction |
SkinFn | | Hole | | rangeSubclass | Object | A UnaryFunction that maps a Hole to the skin of the Hole. The skin of a Hole is the fusion of those superficial parts (see superficialPart) of the Hole's principal host (see PrincipalHostFn) with which the Hole is externally connected | | (=> (equal ?OBJ1 (SkinFn ?HOLE)) (forall (?OBJ2) (<=> (overlapsSpatially ?OBJ2 ?OBJ1) (exists (?OBJ3) (and (superficialPart ?OBJ3 (PrincipalHostFn ?HOLE)) (meetsSpatially ?HOLE ?OBJ3) (overlapsSpatially ?OBJ2 ?OBJ3))))))
| | UnaryFunction |
SquareRootFn | | RealNumber | | rangeSubclass | RealNumber | (SquareRootFn ?NUMBER) is the principal square root of ?NUMBER | | (=> (equal (SquareRootFn ?NUMBER1) ?NUMBER2) (equal (MultiplicationFn ?NUMBER2 ?NUMBER2) ?NUMBER1))
| | UnaryFunction |
SuccessorFn | | Integer | | rangeSubclass | Integer | A UnaryFunction that maps an Integer to its successor, e.g. the successor of 5 is 6 | | (=> (instance ?INT Integer) (lessThan ?INT (SuccessorFn ?INT)))
| | UnaryFunction |
TangentFn | | PlaneAngleMeasure | | rangeSubclass | RealNumber | (TangentFn ?DEGREE) is the tangent of the PlaneAngleMeasure ?DEGREE. The tangent of ?DEGREE is the ratio of the side opposite ?DEGREE to the side next to ?DEGREE in a right-angled triangle | | (equal (TangentFn ?DEGREE) (DivisionFn (SineFn ?DEGREE) (CosineFn ?DEGREE)))
| | UnaryFunction |
TerminalFn | | EngineeringComponent | | rangeSubclass | Terminal | A UnaryFunction that maps an EngineeringComponent to its corresponding Terminal | | (=> (instance ?FUNCTION UnaryFunction) (valence ?FUNCTION 1))
| | UnaryFunction |
TruthFn | TruthValue | Sentence | | rangeSubclass | | The function mapping Sentences to TruthValues | | (=> (instance ?FUNCTION UnaryFunction) (valence ?FUNCTION 1))
| | UnaryFunction |
UnaryConstantFunctionQuantity | | | ConstantQuantity, FunctionQuantity | trichotomizingOn | | The class of UnaryFunctions that map from the Class ConstantQuantity to the Class ConstantQuantity | | (=> (instance ?FUNCTION UnaryConstantFunctionQuantity) (and (domain ?FUNCTION 1 ConstantQuantity) (range ?FUNCTION ConstantQuantity)))
| UnaryFunction | |
WealthFn | | Agent | | rangeSubclass | CurrencyMeasure | A UnaryFunction that maps an Agent to a CurrencyMeasure specifying the value of the property owned by the Agent. Note that this Function is generally used in conjunction with the Function PropertyFn, e.g. (WealthFn (PropertyFn BillGates)) would return the monetary value of the sum of Bill Gates' holdings | | (<=> (equal (WealthFn ?PERSON) ?AMOUNT) (monetaryValue (PropertyFn ?PERSON) ?AMOUNT))
| | UnaryFunction |
WhenFn | | Physical | | rangeSubclass | TimeInterval | A UnaryFunction that maps an Object or Process to the exact TimeInterval during which it exists. Note that, for every TimePoint ?TIME outside of the TimeInterval (WhenFn ?THING), ?THING is not existant at ?TIME | | (starts (ImmediateFutureFn (WhenFn ?THING)) (FutureFn (WhenFn ?THING)))
| | UnaryFunction |
YearFn | | Integer | | rangeSubclass | Year | A UnaryFunction that maps a number to the corresponding calendar Year. For example, (YearFn 1912) denotes the Year 1912 | | (=> (instance ?FUNCTION UnaryFunction) (valence ?FUNCTION 1))
| | UnaryFunction |