This theory provides representation for unary functions which map a scalar-quantity to a scalar-quantity. This type of function is typical in engineering analysis. A common example is a time-dependent-quantity such as 'the temperature reading of my thermometer'. This quantity is a function from a scalar-quantities of dimension time to a scalar-quantity measuring temperature. Although it is common for the 'independent variable' to be time, unary-scalar-function-quantities may be defined over any class of scalar quantities [of a homogenous dimension]. Unary-scalar-function-quantities are quantities themselves, and may be combined with addition, multiplication, and other functions defined for scalar-quantities. In addition, these quantities also have properties such as continuity and can have derivatives.

**Source code: unary-scalar-functions.lisp****List of other known theories**

Physical-QuantitiesFrame-OntologyKif-RelationsKif-SetsKif-ListsKif-NumbersAbstract-AlgebraFrame-Ontology...Standard-UnitsPhysical-Quantities...

CmlThermodynamicsDmeThermodynamics

Relation-Extended-To-Function-QuantitiesTime-QuantityUnary-Scalar-Function-QuantityContinuousTime-Dependent-QuantityTime-Dependent-Quantity

**D/Dt****Deriv****The-Identity-Unary-Scalar-Function-For-Domain****The-Zero-Unary-Scalar-Function-For-Dimension****Value-At**

**The following constants were used from included theories:**

**1-***defined as a***function***in theory***Kif-Numbers****Arity***defined as a***function***in theory***Frame-Ontology****Class***defined as a***class***in theory***Frame-Ontology****Defined***defined as a***class***in theory***Kif-Relations****Documentation***defined as a***relation***in theory***Frame-Ontology****Domain***defined as a***relation***in theory***Frame-Ontology****Exact-Domain***defined as a***function***in theory***Frame-Ontology****Function***defined as a***class***in theory***Kif-Relations****Function***defined as a***class***in theory***Frame-Ontology****Function-Quantity***defined as a***class***in theory***Physical-Quantities****Holds***defined as a***relation***in theory***Kif-Relations****Instance-Of***defined as a***relation***in theory***Frame-Ontology****Item***defined as a***relation***in theory***Kif-Lists****Map***defined as a***function***in theory***Kif-Relations****Member***defined as a***relation***in theory***Kif-Sets****Nth-Domain***defined as a***relation***in theory***Frame-Ontology****Physical-Dimension***defined as a***class***in theory***Physical-Quantities****Physical-Quantity***defined as a***class***in theory***Physical-Quantities****Quantity.Dimension***defined as a***function***in theory***Physical-Quantities****Range***defined as a***relation***in theory***Frame-Ontology****Real-Number***defined as a***class***in theory***Kif-Numbers****Relation***defined as a***class***in theory***Kif-Relations****Relation***defined as a***class***in theory***Frame-Ontology****Subclass-Of***defined as a***relation***in theory***Frame-Ontology****Time-Dimension***defined as a***object***in theory***Standard-Units****Unary-Function***defined as a***class***in theory***Kif-Relations****Unary-Function***defined as a***class***in theory***Frame-Ontology****Value***defined as a***function***in theory***Kif-Relations**

**The following constants were used from theories not included:**

**Identity-Scalar***defined as a***object***in theory***Scalar-Quantities****Scalar-Quantity***defined as a***class***in theory***Scalar-Quantities****The-Zero-Scalar-For-Dimension***defined as a***function***in theory***Scalar-Quantities**

**All constants that were mentioned were defined.**

A unary function that maps from a scalar-quantity to a scalar-quantity.

**Subclass-Of:**Function-quantity, Unary-function

**Domain:**Scalar-quantity**Range:**Scalar-quantity

*Slots Of Instances:*

**Axioms:**

(<=> (Unary-Scalar-Function-Quantity ?X) (And (Function-Quantity ?X) (Unary-Function ?X) (Domain ?X Scalar-Quantity) (Range ?X Scalar-Quantity) ))

**Defined in theory: Unary-scalar-functions****Source code: unary-scalar-functions.lisp**

The function value-at returns the value of a quantity at some point in 'time' (or whatever the independent state variable is). The 'time' argument is just a constant scalar-quantity, such as a time-quantity. If the quantity is a function-quantity, then its value-at is its function value applied to the 'time' argument. If the quantity is constant-quantity, then its value-at is the quantity itself for all 'times'.

**Arity:**3

**Axioms:**

(Nth-Domain Value-At 2 Scalar-Quantity) (Nth-Domain Value-At 1 Physical-Quantity) (=> (Value-At ?Q ?Time ?Val) (And (Physical-Quantity ?Q) (Scalar-Quantity ?Time)) ) (= (Value-At ?Q ?Time) (If (Function-Quantity ?Q) (Value ?Q ?Time) ?Q) )

**Defined in theory: Unary-scalar-functions****Source code: unary-scalar-functions.lisp****Also defined in:**Cml

A relation-extended-to-function-quantities is a relation that is defined for both constant-quantities and unary-scalar-function-quantities. The relation holds on some arguments (which may be function-quantities), if and only if whenever all the arguments have a value-at some ?t, the relation holds on those values. The relation may be of any arity. Since value-at is defined for both function-quantities and constant-quantities, a relation-extended-to-function-quantities can be defined on sequences of arguments that are mixes of function-quantities and constant-quantities.For example, the inequality relation

<is a relation-extended-to-function-quantities. Consider the case of (<?x ?y). Whenever (value-at ?x ?t) is defined and (value-at ?y ?t) is defined, then (<(value-at ?x ?t) (value-at ?y ?t)). There can be some ?t for which ?x or ?y is undefined, as long as for those ?t on which they are both defined, they<relation holds on their values. Either ?x or ?y or both can be constant-quantities, since (value-at ?x ?t) is just ?x when ?x is a constant.Since functions are relations, a function may also be extended to apply to function quantities. The same axioms hold. Intuitively, a the value of a function F over function-quantities qf1 and qf2 is another quantity-function (F qf1 qf2) such that for all ?t where (qf1 ?t) and (qf2 ?t) are defined, (F qf1 qf2) = (F (qf1 ?t) (qf2 ?t)).

**Subclass-Of:**Relation

**Axioms:**

(<=> (Relation-Extended-To-Function-Quantities ?R) (Forall (@Args) (<=> (Holds ?R @Args) (Forall (?T) (=> (=> (Item ?Q (Listof @Args)) (Defined (Value-At ?Q ?T)) ) (Member (Map (Lambda (?Q) (Value-At ?Q ?T) ) (Listof @Args) ) ?R))))))

**Defined in theory: Unary-scalar-functions****Source code: unary-scalar-functions.lisp**

**Instance-Of:**Sentence**Defining-Axiom:**'(<=> (Holds ?R ?Q1 ?Q2) (Forall (?T) (=> (And (Defined (Value-At ?Q1 ?T)) (Defined (Value-At ?Q2 ?T)) ) (Holds ?R (Value-At ?Q1 ?T) (Value-At ?Q2 ?T)) )))

**Defined in theory: Unary-scalar-functions***No source file available.*

The the-identity-unary-scalar-function-for-domain is a scalar function which has a range = 1 for the exact-domain ?domain; f(x) = 1 forall x in ?domain.

**Arity:**2**Range:**Unary-scalar-function-quantity

**Axioms:**

(=> (The-Identity-Unary-Scalar-Function-For-Domain ?Domain ?F) (And (Subclass-Of ?Domain Scalar-Quantity) (Exact-Domain ?F ?Domain) (Forall (?T) (=> (Instance-Of ?T ?Domain) (= (Value ?F ?T) Identity-Scalar) ))))

**Defined in theory: Unary-scalar-functions****Source code: unary-scalar-functions.lisp**

The zero-usf-function is the scalar function that has a range = zero-scalar-for-dimension ?physdim for exact-domain ?domain; f(x)=0 forall x in ?domain.

**Arity:**3

**Axioms:**

(Nth-Domain The-Zero-Unary-Scalar-Function-For-Dimension 3 Unary-Scalar-Function-Quantity) (Nth-Domain The-Zero-Unary-Scalar-Function-For-Dimension 1 Physical-Dimension) (=> (The-Zero-Unary-Scalar-Function-For-Dimension ?Physdim ?Domain ?F) (And (Subclass-Of ?Domain Scalar-Quantity) (Exact-Domain ?F ?Domain) (Forall (?T) (=> (Instance-Of ?T ?Domain) (= (Value ?F ?T) (The-Zero-Scalar-For-Dimension ?Physdim) )))))

**Defined in theory: Unary-scalar-functions****Source code: unary-scalar-functions.lisp**

Relation defining functions which are continuous. This concept is taken as primitive until representations for limits are generated.

**Subclass-Of:**Unary-scalar-function-quantity

**Defined in theory: Unary-scalar-functions****Source code: unary-scalar-functions.lisp**

deriv[?x] is the derivative of unary-scalar-function-quantity ?x {deriv[f[x]] = f'[x]}. Deriv is only defined on continuous functions.

Deriv has the normal algebraic properties of derivatives of real-valued functions; see the axioms for the exact behavior of differentiation with respect to sums and products of unary-scalar-function-quantities.

**Arity:**2**Domain:**Continuous, Unary-scalar-function-quantity**Range:**Unary-scalar-function-quantity

**Axioms:**

(Forall (?F ?G ?R) (=> (And (Unary-Scalar-Function-Quantity ?F) (Unary-Scalar-Function-Quantity ?G) (Real-Number ?R) ) (And (= (Deriv (+ ?F ?G)) (+ (Deriv ?F) (Deriv ?G))) (= (Deriv (* ?F ?G)) (+ (* (Deriv ?F) ?G) (* ?F (Deriv ?G))) ) (= (Deriv (Expt ?F ?R)) (* ?R (Expt (Deriv ?F) (1- ?R))) ))))

**Defined in theory: Unary-scalar-functions****Source code: unary-scalar-functions.lisp**

A time-quantity is a scalar quantity whose dimension is time-dimension. Conceptually, a time-quantity is an amount [duration] of time. It is constant quantity, not a function or an interval. Like all constant-quantities, its magnitude is given in terms of units of measure. For example, the products of all real numbers and a unit like second-of-time are time quantities.

**Subclass-Of:**Scalar-quantity

**Quantity.Dimension:**Time-dimension

*Slots Of Instances:*

**Axioms:**

(<=> (Time-Quantity ?T) (And (Scalar-Quantity ?T) (= (Quantity.Dimension ?T) Time-Dimension) ))

**Defined in theory: Unary-scalar-functions****Source code: unary-scalar-functions.lisp**

A unary scalar function of continuous time. Maps a time-quantity into another scalar quantity such as a temperature. For example, a quantity that denotes 'the temperature of the top of the Empire State Building' is a time-dependent-quantity since its value depends on the time.

**Subclass-Of:**Continuous, Unary-scalar-function-quantity

**Axioms:**

(<=> (Time-Dependent-Quantity ?X) (And (Unary-Scalar-Function-Quantity ?X) (Continuous ?X) (Subclass-Of (Exact-Domain ?X) Time-Quantity) ))

**Defined in theory: Unary-scalar-functions****Source code: unary-scalar-functions.lisp**

(D/DT ?q) is the derivative with respect to time of the

time-dependent-quantity ?q. It is undefined on other quantities, including constant-quantities.

**Arity:**2

**Axioms:**

(= (D/Dt ?Q) (If (Time-Quantity ?Q) (Deriv ?Q)))

**Defined in theory: Unary-scalar-functions****Source code: unary-scalar-functions.lisp**

Formatting and translation code was written by