Relation DIMENSION-COMPOSABLE-FROM

• Defined in theory: Physical-quantities
• Source code: physical-quantities.lisp

Slots on this relation:

Instance-Of: Relation

Arity: 2

Domain: Physical-dimension

Equivalence Axioms:

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

Other Related Axioms:

(=> (Member ?Dim ?Set-Of-Dimensions)
    (And (Physical-Dimension ?Dim)
         (Not (Dimension-Composable-From ?Dim
                                         (Difference 
                                             ?Set-Of-Dimensions
                                             (Setof ?Dim))))))

(<=> (Orthogonal-Dimension-Set ?Set-Of-Dimensions)
     (And (Simple-Set ?Set-Of-Dimensions)
          (=> (Member ?Dim ?Set-Of-Dimensions)
              (And (Physical-Dimension ?Dim)
                   (Not (Dimension-Composable-From 
                            ?Dim
                            (Difference ?Set-Of-Dimensions
                                        (Setof ?Dim))))))))

(=> (Dimension-Composable-From $X $Y) (Physical-Dimension $X))

(=> (Dimension-Composable-From ?Dim ?Set-Of-Dimensions)
    (=> (Member ?Dim ?Set-Of-Dimensions) (Physical-Dimension ?Dim)))

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