Function EXPT

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

Slots on this function:

Documentation:

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

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

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

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

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