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