Function EXPT

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

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.

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

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:

(= (Recip ?X) (Expt ?X -1))

(=> (And (Physical-Quantity ?X) (Recip ?X ?Y))
    (And (Physical-Quantity ?Y)
         (= (Quantity.Dimension ?Y)
            (Expt (Quantity.Dimension ?X) -1))))

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

(=> (And (Physical-Quantity ?X) (Physical-Quantity ?Y))
    (= (/ ?X ?Y) (* ?X (Expt ?Y -1))))

(=> (And (Unit-Of-Measure ?A) (Real-Number ?B))
    (Unit-Of-Measure (Expt ?A ?B)))

(<=> (Dimension-Composable-From ?Dim ?Set-Of-Dimensions)
     (Or (Member ?Dim ?Set-Of-Dimensions)
         (Exists (?Dim1 ?Dim2)
                 (And (Dimension-Composable-From ?Dim1
                                                 ?Set-Of-Dimensions)
                      (Dimension-Composable-From ?Dim2
                                                 ?Set-Of-Dimensions)
                      (= ?Dim (* ?Dim1 ?Dim2))))
         (Exists (?Dim1 ?Real)
                 (And (Dimension-Composable-From ?Dim1
                                                 ?Set-Of-Dimensions)
                      (Real-Number ?Real)
                      (= ?Dim (Expt ?Dim1 ?Real))))))