Relation COMPATIBLE-QUANTITIES

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

Slots on this relation:

Documentation:

Two physical quantities are compatible if their physical-dimensions are equal. Compatibility constrains how quantities can be compared and combined with algebraic operators.

Instance-Of: Relation

Arity: 2

Domain: Physical-quantity

Range: Physical-quantity

Equivalence Axioms:

(<=> (Compatible-Quantities ?X ?Y)
     (And (Physical-Quantity ?X)
          (Physical-Quantity ?Y)
          (= (Quantity.Dimension ?X) (Quantity.Dimension ?Y))))

Other Related Axioms:

(=> (Compatible-Quantities $X $Y) (Physical-Quantity $Y))

(=> (Compatible-Quantities $X $Y) (Physical-Quantity $X))

(<=> (Compatible-Quantities ?X ?Y)
     (And (Physical-Quantity ?X)
          (Physical-Quantity ?Y)
          (= (Quantity.Dimension ?X) (Quantity.Dimension ?Y))))

(=> (= (Magnitude ?Q ?Unit) ?Mag) (Compatible-Quantities ?Q ?Unit))

(=> (And (Physical-Quantity ?X) (Physical-Quantity ?Y) (+ ?X ?Y ?Z))
    (And (Physical-Quantity ?Z)
         (Compatible-Quantities ?X ?Y)
         (Compatible-Quantities ?X ?Z)))

(Forall (@Args)
        (<=> (And (Holds ?R @Args)
                  (=> (Item ?Q (Listof @Args))
                      (Constant-Quantity ?Q)))
             (Forall (?Unit ?Q)
                     (=> (And (Unit-Of-Measure ?Unit)
                              (=> (Item ?Q (Listof @Args))
                                  (Compatible-Quantities ?Q ?Unit)))
                         (Member (Map (Lambda (?Q)
                                              (Magnitude ?Q ?Unit))
                                      (Listof @Args))
                                 ?R)))))

(<=> (Relation-Extended-To-Quantities ?R)
     (And (Relation ?R)
          (Forall (@Args)
                  (<=> (And (Holds ?R @Args)
                            (=> (Item ?Q (Listof @Args))
                                (Constant-Quantity ?Q)))
                       (Forall (?Unit ?Q)
                               (=> (And (Unit-Of-Measure ?Unit)
                                        (=> (Item ?Q (Listof @Args))
                                            (Compatible-Quantities 
                                                ?Q
                                                ?Unit)))
                                   (Member (Map (Lambda 
                                                    (?Q)
                                                    (Magnitude ?Q
                                                               ?Unit))
                                                (Listof @Args))
                                           ?R)))))))

(Forall (?Other-Unit)
        (=> (And (Unit-Of-Measure ?Other-Unit)
                 (Compatible-Quantities ?U ?Other-Unit))
            (And (Real-Number (Magnitude ?U ?Other-Unit))
                 (Positive (Magnitude ?U ?Other-Unit)))))

(<=> (Unit-Of-Measure ?U)
     (And (Constant-Quantity ?U)
          (Forall (?Other-Unit)
                  (=> (And (Unit-Of-Measure ?Other-Unit)
                           (Compatible-Quantities ?U ?Other-Unit))
                      (And (Real-Number (Magnitude ?U ?Other-Unit))
                           (Positive (Magnitude ?U ?Other-Unit)))))))

Notes:

• EXAMPLE
• Compatible-Quantities: (* 6 feet)
  

  (* 20 meters)