[1] | 1 | \begin{lisp:documentation}{*prover$-$order*}{VARIABLE}{\#'grevlex$>$ }
|
---|
| 2 | Admissible monomial order used internally in the proofs of theorems.
|
---|
| 3 | \end{lisp:documentation}
|
---|
| 4 |
|
---|
| 5 | \begin{lisp:documentation}{csym}{FUNCTION}{symbol number }
|
---|
| 6 | Return symbol whose name is a concatenation of (SYMBOL$-$NAME SYMBOL)
|
---|
| 7 | and a number NUMBER.
|
---|
| 8 | \end{lisp:documentation}
|
---|
| 9 |
|
---|
| 10 | \begin{lisp:documentation}{real$-$identical$-$points}{MACRO}{a b }
|
---|
| 11 | Return [ (A1$-$B1)**2 + (A2$-$B2)**2 ] in lisp (prefix) notation.
|
---|
| 12 | The second value is the list of variables (A1 B1 A2 B2). Note that
|
---|
| 13 | if the distance between two complex points A, B is zero, it does not
|
---|
| 14 | mean that the points are identical. Use IDENTICAL$-$POINTS to express
|
---|
| 15 | the fact that A and B are really identical. Use this macro in
|
---|
| 16 | conclusions of theorems, as it may not be possible to prove that A
|
---|
| 17 | and B are trully identical in the complex domain.
|
---|
| 18 | \end{lisp:documentation}
|
---|
| 19 |
|
---|
| 20 | \begin{lisp:documentation}{identical$-$points}{MACRO}{a b }
|
---|
| 21 | Return [ A1$-$B1, A2$-$B2 ] in lisp (prefix) notation.
|
---|
| 22 | The second value is the list of variables (A1 B1 A2 B2). Note that
|
---|
| 23 | sometimes one is able to prove only that (A1$-$B1)**2 + (A2$-$B2)**2
|
---|
| 24 | = 0. This equation in the complex domain has solutions with A and B
|
---|
| 25 | distinct. Use REAL$-$IDENTICAL$-$POINTS to express the fact that the
|
---|
| 26 | distance between two points is 0. Use this macro in assumptions of
|
---|
| 27 | theorems, although this is seldom necessary because we assume most of
|
---|
| 28 | the time that in assumptions all points are distinct if they are
|
---|
| 29 | denoted by different symbols.
|
---|
| 30 | \end{lisp:documentation}
|
---|
| 31 |
|
---|
| 32 | \begin{lisp:documentation}{perpendicular}{MACRO}{a b c d }
|
---|
| 33 | Return [ (A1$-$B1) * (C1$-$D1) + (A2$-$B2) * (C2$-$D2) ] in lisp
|
---|
| 34 | (prefix) notation. The second value is the list of variables (A1 A2
|
---|
| 35 | B1 B2 C1 C2 D1 D2).
|
---|
| 36 | \end{lisp:documentation}
|
---|
| 37 |
|
---|
| 38 | \begin{lisp:documentation}{parallel}{MACRO}{a b c d }
|
---|
| 39 | Return [ (A1$-$B1) * (C2$-$D2) $-$ (A2$-$B2) * (C1$-$D1) ] in lisp
|
---|
| 40 | (prefix) notation. The second value is the list of variables (A1 A2
|
---|
| 41 | B1 B2 C1 C2 D1 D2).
|
---|
| 42 | \end{lisp:documentation}
|
---|
| 43 |
|
---|
| 44 | \begin{lisp:documentation}{collinear}{MACRO}{a b c }
|
---|
| 45 | Return the determinant det([[A1,A2,1],[B1,B2,1],[C1,C2,1]]) in lisp
|
---|
| 46 | (prefix) notation. The second value is the list of variables (A1 A2
|
---|
| 47 | B1 B2 C1 C2).
|
---|
| 48 | \end{lisp:documentation}
|
---|
| 49 |
|
---|
| 50 | \begin{lisp:documentation}{equidistant}{MACRO}{a b c d }
|
---|
| 51 | Return the polynomial
|
---|
| 52 | [(A1$-$B1)**2+(A2$-$B2)**2$-$(C1$-$D1)**2$-$(C2$-$D2)**2] in lisp
|
---|
| 53 | (prefix) notation. The second value is the list of variables (A1 A2
|
---|
| 54 | B1 B2 C1 C2 D1 D2).
|
---|
| 55 | \end{lisp:documentation}
|
---|
| 56 |
|
---|
| 57 | \begin{lisp:documentation}{euclidean$-$distance}{MACRO}{a b r }
|
---|
| 58 | Return the polynomial [(A1$-$B1)**2+(A2$-$B2)**2$-$R\symbol{94}2] in
|
---|
| 59 | lisp (prefix) notation. The second value is the list of variables (A1
|
---|
| 60 | A2 B1 B2 R).
|
---|
| 61 | \end{lisp:documentation}
|
---|
| 62 |
|
---|
| 63 | \begin{lisp:documentation}{midpoint}{MACRO}{a b c }
|
---|
| 64 | Express the fact that C is a midpoint of the segment AB.
|
---|
| 65 | Returns the list [ 2*C1$-$A1$-$B1, 2*C2$-$A2$-$B2 ]. The second value
|
---|
| 66 | returned is the list of variables (A1 A2 B1 B2 C1 C2).
|
---|
| 67 | \end{lisp:documentation}
|
---|
| 68 |
|
---|
| 69 | \begin{lisp:documentation}{translate$-$statements}{MACRO}{{\sf \&rest} statements }
|
---|
| 70 | {\ } % NO DOCUMENTATION FOR TRANSLATE-STATEMENTS
|
---|
| 71 | \end{lisp:documentation}
|
---|
| 72 |
|
---|
| 73 | \begin{lisp:documentation}{translate$-$assumptions}{MACRO}{{\sf \&rest} assumptions }
|
---|
| 74 | {\ } % NO DOCUMENTATION FOR TRANSLATE-ASSUMPTIONS
|
---|
| 75 | \end{lisp:documentation}
|
---|
| 76 |
|
---|
| 77 | \begin{lisp:documentation}{translate$-$conclusions}{MACRO}{{\sf \&rest} conclusions }
|
---|
| 78 | {\ } % NO DOCUMENTATION FOR TRANSLATE-CONCLUSIONS
|
---|
| 79 | \end{lisp:documentation}
|
---|
| 80 |
|
---|
| 81 | \begin{lisp:documentation}{translate$-$theorem}{MACRO}{({\sf \&rest} assumptions) ({\sf \&rest} conclusions) }
|
---|
| 82 | Translates a planar geometry theorem into a system of polynomial
|
---|
| 83 | equations. Each assumption or conclusion takes form of a declaration
|
---|
| 84 | (RELATION$-$NAME A B C ...) where A B C are points, entered as
|
---|
| 85 | symbols and RELATION$-$NAME is a name of a geometric relation, for
|
---|
| 86 | example, (COLLINEAR A B C) means that points A, B, C are all
|
---|
| 87 | collinear. The translated equations use the convention that (A1,A2)
|
---|
| 88 | are the coordinates of the point A. This macro returns multiple
|
---|
| 89 | values. The first value is a list of polynomial expressions and the
|
---|
| 90 | second value is an automatically generated list of variables from
|
---|
| 91 | points A, B, C, etc. For convenience, several macros have been
|
---|
| 92 | defined in order to make specifying common geometric relations easy.
|
---|
| 93 | \end{lisp:documentation}
|
---|
| 94 |
|
---|
| 95 | \begin{lisp:documentation}{prove$-$theorem}{MACRO}{({\sf \&rest} assumptions) ({\sf \&rest} conclusions) {\sf \&key} (order *prover$-$order*) }
|
---|
| 96 | Proves a geometric theorem, specified in the same manner as in
|
---|
| 97 | the macro TRANSLATE$-$THEOREM. The proof is achieved by a call to
|
---|
| 98 | IDEAL$-$POLYSATURATION. The theorem is true if the returned value
|
---|
| 99 | is a trivial ideal containing 1.
|
---|
| 100 | \end{lisp:documentation}
|
---|
| 101 |
|
---|