Function EXPT

• Defined in theory: Unary-scalar-functions
• Source code: unary-scalar-functions.lisp
• Also defined in: Kif-numbers, Dme-kb, Physical-quantities, Scalar-quantities

Slots on this function:

Documentation:

EXPT defines real exponentiation for scalar-quantities. Specializes EXPT.

and also:

EXPT is exponentiation. It is defined for numbers in the kif-numbers ontology. Here it is extended to physical quantities and physical dimensions.

and also:

Real exponentiation for unary-scalar-function-quantitys.

and also:

{The term {tt (expt $tau_1$ $tau_2$)} denotes the object denoted by
$tau_1$ raised to the power the object denoted by $tau_2$.}

Instance-Of: Function, Relation-extended-to-function-quantities

Arity: 3

Implication Axioms:

(=> (And (Physical-Dimension ?D)
         (Real-Number ?Exp)
         (Expt ?D ?Exp ?Dim))
    (Physical-Dimension ?Dim))

(=> (And (Physical-Quantity ?X) (Real-Number ?R) (Expt ?X ?R ?Z))
    (And (Physical-Quantity ?Z)
         (= (Quantity.Dimension ?Z)
            (Expt (Quantity.Dimension ?X) ?R))))

(=> (And (Physical-Dimension ?D)
         (Real-Number ?Exp)
         (Expt ?D ?Exp ?Dim))
    (Physical-Dimension ?Dim))

(=> (And (Physical-Quantity ?X) (Real-Number ?R) (Expt ?X ?R ?Z))
    (And (Physical-Quantity ?Z)
         (= (Quantity.Dimension ?Z)
            (Expt (Quantity.Dimension ?X) ?R))))

(=> (And (Scalar-Quantity ?X) (Real-Number ?R) (Expt ?X ?R ?Z))
    (And (Scalar-Quantity ?Z)
         (=> (= ?R 0) (= ?Z 1))
         (Forall (?U)
                 (=> (Unit-Of-Measure ?U)
                     (= (Expt (Magnitude ?X ?U) ?R)
                        (Magnitude ?Z (Expt ?U ?R)))))))

(=> (And (Unary-Scalar-Function-Quantity ?X)
         (Real-Number ?R)
         (Expt ?X ?R ?Z))
    (Unary-Scalar-Function-Quantity ?Z))

Axioms:

(Forall (?D1 ?D2 ?R1 ?R2)
        (=> (And (Physical-Dimension ?D1)
                 (Physical-Dimension ?D2)
                 (Real-Number ?R1)
                 (Real-Number ?R2))
            (And (= (Expt ?D1 0) Identity-Dimension)
                 (= ?D1 (Expt ?D1 1))
                 (= (* (Expt ?D1 ?R1) (Expt ?D1 ?R2))
                    (Expt ?D1 (+ ?R1 ?R2)))
                 (= (Expt (* ?D1 ?D2) ?R1)
                    (* (Expt ?D1 ?R1) (Expt ?D2 ?R1)))
                 (= (Expt (Expt ?D1 ?R1) ?R2) (Expt ?D1 (* ?R1 ?R2))))))

(Forall (?X1 ?X2 ?R1 ?R2)
        (=> (And (Physical-Quantity ?X1)
                 (Physical-Quantity ?X2)
                 (Real-Number ?R1)
                 (Real-Number ?R2))
            (And (= (* (Expt ?X1 ?R1) (Expt ?X1 ?R2))
                    (Expt ?X1 (+ ?R1 ?R2)))
                 (= (Expt (* ?X1 ?X2) ?R1)
                    (* (Expt ?X1 ?R1) (Expt ?X2 ?R1)))
                 (= (Expt (Expt ?X1 ?R1) ?R2) (Expt ?X1 (* ?R1 ?R2))))))

(Forall (?D1 ?D2 ?R1 ?R2)
        (=> (And (Physical-Dimension ?D1)
                 (Physical-Dimension ?D2)
                 (Real-Number ?R1)
                 (Real-Number ?R2))
            (And (= (Expt ?D1 0) Identity-Dimension)
                 (= ?D1 (Expt ?D1 1))
                 (= (* (Expt ?D1 ?R1) (Expt ?D1 ?R2))
                    (Expt ?D1 (+ ?R1 ?R2)))
                 (= (Expt (* ?D1 ?D2) ?R1)
                    (* (Expt ?D1 ?R1) (Expt ?D2 ?R1)))
                 (= (Expt (Expt ?D1 ?R1) ?R2) (Expt ?D1 (* ?R1 ?R2))))))

(Forall (?X1 ?X2 ?R1 ?R2)
        (=> (And (Physical-Quantity ?X1)
                 (Physical-Quantity ?X2)
                 (Real-Number ?R1)
                 (Real-Number ?R2))
            (And (= (* (Expt ?X1 ?R1) (Expt ?X1 ?R2))
                    (Expt ?X1 (+ ?R1 ?R2)))
                 (= (Expt (* ?X1 ?X2) ?R1)
                    (* (Expt ?X1 ?R1) (Expt ?X2 ?R1)))
                 (= (Expt (Expt ?X1 ?R1) ?R2) (Expt ?X1 (* ?R1 ?R2))))))

Other Related Axioms:

(=> (And (Unary-Scalar-Function-Quantity ?X)
         (Real-Number ?R)
         (Expt ?X ?R ?Z))
    (Unary-Scalar-Function-Quantity ?Z))

(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)))))))