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