source: CGBLisp/doc/prover.txt@ 1

;;; *PROVER-ORDER* (#'grevlex>)                                      [VARIABLE]
;;;    Admissible monomial order used internally in the proofs of theorems.
;;;
;;; CSYM (symbol number)                                             [FUNCTION]
;;;    Return symbol whose name is a concatenation of (SYMBOL-NAME SYMBOL)
;;;    and a number NUMBER.
;;;
;;; REAL-IDENTICAL-POINTS (a b)                                         [MACRO]
;;;    Return [ (A1-B1)**2 + (A2-B2)**2 ] in lisp (prefix) notation.
;;;    The second value is the list of variables (A1 B1 A2 B2). Note that
;;;    if the distance between two complex points A, B is zero, it does not
;;;    mean that the points are identical. Use IDENTICAL-POINTS to express
;;;    the fact that A and B are really identical. Use this macro in
;;;    conclusions of theorems, as it may not be possible to prove that A
;;;    and B are trully identical in the complex domain.
;;;
;;; IDENTICAL-POINTS (a b)                                              [MACRO]
;;;    Return [ A1-B1, A2-B2 ] in lisp (prefix) notation.
;;;    The second value is the list of variables (A1 B1 A2 B2). Note that
;;;    sometimes one is able to prove only that (A1-B1)**2 + (A2-B2)**2 = 0.
;;;    This equation in the complex domain has solutions with A and B
;;;    distinct. Use REAL-IDENTICAL-POINTS to express the fact that the
;;;    distance between two points is 0. Use this macro in assumptions of
;;;    theorems, although this is seldom necessary because we assume most of
;;;    the time that in assumptions all points are distinct if they are
;;;    denoted by different symbols. 
;;;
;;; PERPENDICULAR (a b c d)                                             [MACRO]
;;;    Return [ (A1-B1) * (C1-D1) + (A2-B2) * (C2-D2) ] in lisp (prefix)
;;;    notation. The second value is the list of variables (A1 A2 B1 B2 C1
;;;    C2 D1 D2). 
;;;
;;; PARALLEL (a b c d)                                                  [MACRO]
;;;    Return [ (A1-B1) * (C2-D2) - (A2-B2) * (C1-D1) ] in lisp (prefix)
;;;    notation. The second value is the list of variables (A1 A2 B1 B2 C1
;;;    C2 D1 D2). 
;;;
;;; COLLINEAR (a b c)                                                   [MACRO]
;;;    Return the determinant det([[A1,A2,1],[B1,B2,1],[C1,C2,1]]) in lisp
;;;    (prefix) notation. The second value is the list of variables (A1 A2
;;;    B1 B2 C1 C2). 
;;;
;;; EQUIDISTANT (a b c d)                                               [MACRO]
;;;    Return the polynomial [(A1-B1)**2+(A2-B2)**2-(C1-D1)**2-(C2-D2)**2]
;;;    in lisp (prefix) notation. The second value is the list of variables
;;;    (A1 A2 B1 B2 C1 C2 D1 D2). 
;;;
;;; EUCLIDEAN-DISTANCE (a b r)                                          [MACRO]
;;;    Return the polynomial [(A1-B1)**2+(A2-B2)**2-R^2] in lisp (prefix)
;;;    notation. The second value is the list of variables (A1 A2 B1 B2 R).
;;;
;;; MIDPOINT (a b c)                                                    [MACRO]
;;;    Express the fact that C is a midpoint of the segment AB.
;;;    Returns the list [ 2*C1-A1-B1, 2*C2-A2-B2 ]. The second value
;;;    returned is the list of variables (A1 A2 B1 B2 C1 C2).
;;;
;;; TRANSLATE-STATEMENTS (&rest statements)                             [MACRO]
;;;
;;; TRANSLATE-ASSUMPTIONS (&rest assumptions)                           [MACRO]
;;;
;;; TRANSLATE-CONCLUSIONS (&rest conclusions)                           [MACRO]
;;;
;;; TRANSLATE-THEOREM ((&rest assumptions) (&rest conclusions))         [MACRO]
;;;    Translates a planar geometry theorem into a system of polynomial
;;;    equations. Each assumption or conclusion takes form of a declaration
;;;    (RELATION-NAME A B C ...) where A B C are points, entered as symbols
;;;    and RELATION-NAME is a name of a geometric relation, for example,
;;;    (COLLINEAR A B C) means that points A, B, C are all collinear. The
;;;    translated equations use the convention that (A1,A2) are the
;;;    coordinates of the point A. This macro returns multiple values. The
;;;    first value is a list of polynomial expressions and the second value
;;;    is an automatically generated list of variables from points A, B, C,
;;;    etc. For convenience, several macros have been defined in order to
;;;    make specifying common geometric relations easy. 
;;;
;;; PROVE-THEOREM ((&rest assumptions) (&rest conclusions)              [MACRO]
;;;                &key (order *prover-order*))
;;;    Proves a geometric theorem, specified in the same manner as in
;;;    the macro TRANSLATE-THEOREM. The proof is achieved by a call to
;;;    IDEAL-POLYSATURATION. The theorem is true if the returned value
;;;    is a trivial ideal containing 1.
;;;