Function EXPT

• Defined in theory: Scalar-quantities
• Source code: scalar-quantities.lisp
• Also defined in: Kif-numbers, Dme-kb, Unary-scalar-functions, Physical-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:

{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

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

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

Other Related Axioms:

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