source: CGBLisp/latex-doc/manual/node8.html@ 1

Last change on this file since 1 was 1, checked in by Marek Rychlik, 15 years ago

First import of a version circa 1997.
File size: 12.8 KB
Line 
1<!--Converted with LaTeX2HTML 97.1 (release) (July 13th, 1997)
2 by Nikos Drakos (nikos@cbl.leeds.ac.uk), CBLU, University of Leeds
3* revised and updated by: Marcus Hennecke, Ross Moore, Herb Swan
4* with significant contributions from:
5 Jens Lippman, Marek Rouchal, Martin Wilck and others -->
6<HTML>
7<HEAD>
8<TITLE>The Geometric Theorem Prover package</TITLE>
9<META NAME="description" CONTENT="The Geometric Theorem Prover package">
10<META NAME="keywords" CONTENT="manual">
11<META NAME="resource-type" CONTENT="document">
12<META NAME="distribution" CONTENT="global">
13<META HTTP-EQUIV="Content-Type" CONTENT="text/html; charset=iso_8859_1">
14<LINK REL="STYLESHEET" HREF="manual.css">
15<LINK REL="next" HREF="node9.html">
16<LINK REL="previous" HREF="node7.html">
17<LINK REL="up" HREF="manual.html">
18<LINK REL="next" HREF="node9.html">
19</HEAD>
20<BODY bgcolor="#ffffff">
21<!--Navigation Panel-->
22<A NAME="tex2html989"
23 HREF="node9.html">
24<IMG WIDTH="37" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="next" SRC="next_motif.gif"></A>
25<A NAME="tex2html986"
26 HREF="manual.html">
27<IMG WIDTH="26" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="up" SRC="up_motif.gif"></A>
28<A NAME="tex2html980"
29 HREF="node7.html">
30<IMG WIDTH="63" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="previous" SRC="previous_motif.gif"></A>
31<A NAME="tex2html988"
32 HREF="node1.html">
33<IMG WIDTH="65" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="contents" SRC="contents_motif.gif"></A>
34<BR>
35<B> Next:</B> <A NAME="tex2html990"
36 HREF="node9.html">The Monomial Order Package</A>
37<B> Up:</B> <A NAME="tex2html987"
38 HREF="manual.html">CGBLisp User Guide and</A>
39<B> Previous:</B> <A NAME="tex2html981"
40 HREF="node7.html">The Dynamical Systems package</A>
41<BR>
42<BR>
43<!--End of Navigation Panel-->
44<!--Table of Child-Links-->
45<A NAME="CHILD_LINKS"><strong>Subsections</strong></A>
46<UL>
47<LI><A NAME="tex2html991"
48 HREF="node8.html#SECTION00080010000000000000">
49<I>*prover<MATH CLASS="INLINE">
50-
51</MATH>order*</I></A>
52<LI><A NAME="tex2html992"
53 HREF="node8.html#SECTION00080020000000000000">
54<I>csym</I></A>
55<LI><A NAME="tex2html993"
56 HREF="node8.html#SECTION00080030000000000000">
57<I>real<MATH CLASS="INLINE">
58-
59</MATH>identical<MATH CLASS="INLINE">
60-
61</MATH>points</I></A>
62<LI><A NAME="tex2html994"
63 HREF="node8.html#SECTION00080040000000000000">
64<I>identical<MATH CLASS="INLINE">
65-
66</MATH>points</I></A>
67<LI><A NAME="tex2html995"
68 HREF="node8.html#SECTION00080050000000000000">
69<I>perpendicular</I></A>
70<LI><A NAME="tex2html996"
71 HREF="node8.html#SECTION00080060000000000000">
72<I>parallel</I></A>
73<LI><A NAME="tex2html997"
74 HREF="node8.html#SECTION00080070000000000000">
75<I>collinear</I></A>
76<LI><A NAME="tex2html998"
77 HREF="node8.html#SECTION00080080000000000000">
78<I>equidistant</I></A>
79<LI><A NAME="tex2html999"
80 HREF="node8.html#SECTION00080090000000000000">
81<I>euclidean<MATH CLASS="INLINE">
82-
83</MATH>distance</I></A>
84<LI><A NAME="tex2html1000"
85 HREF="node8.html#SECTION000800100000000000000">
86<I>midpoint</I></A>
87<LI><A NAME="tex2html1001"
88 HREF="node8.html#SECTION000800110000000000000">
89<I>translate<MATH CLASS="INLINE">
90-
91</MATH>statements</I></A>
92<LI><A NAME="tex2html1002"
93 HREF="node8.html#SECTION000800120000000000000">
94<I>translate<MATH CLASS="INLINE">
95-
96</MATH>assumptions</I></A>
97<LI><A NAME="tex2html1003"
98 HREF="node8.html#SECTION000800130000000000000">
99<I>translate<MATH CLASS="INLINE">
100-
101</MATH>conclusions</I></A>
102<LI><A NAME="tex2html1004"
103 HREF="node8.html#SECTION000800140000000000000">
104<I>translate<MATH CLASS="INLINE">
105-
106</MATH>theorem</I></A>
107<LI><A NAME="tex2html1005"
108 HREF="node8.html#SECTION000800150000000000000">
109<I>prove<MATH CLASS="INLINE">
110-
111</MATH>theorem</I></A>
112</UL>
113<!--End of Table of Child-Links-->
114<HR>
115<H1><A NAME="SECTION00080000000000000000">
116The Geometric Theorem Prover package</A>
117</H1>
118<H4><A NAME="SECTION00080010000000000000">
119<I>*prover<MATH CLASS="INLINE">
120-
121</MATH>order*</I></A>
122</H4>
123<P><IMG WIDTH="510" HEIGHT="29" ALIGN="MIDDLE" BORDER="0"
124 SRC="img138.gif"
125 ALT="$\textstyle\parbox{\pboxargslen}{\em \char93 'grevlex$\gt$\space \/}$"> [<EM>VARIABLE</EM>]
126<BLOCKQUOTE>
127Admissible monomial order used internally in the proofs of theorems.</BLOCKQUOTE><H4><A NAME="SECTION00080020000000000000">
128<I>csym</I></A>
129</H4>
130<P><IMG WIDTH="577" HEIGHT="29" ALIGN="MIDDLE" BORDER="0"
131 SRC="img139.gif"
132 ALT="$\textstyle\parbox{\pboxargslen}{\em symbol number \/}$"> [<EM>FUNCTION</EM>]
133<BLOCKQUOTE>
134Return symbol whose name is a concatenation of (SYMBOL<MATH CLASS="INLINE">
135-
136</MATH>NAME SYMBOL)
137and a number NUMBER.</BLOCKQUOTE><H4><A NAME="SECTION00080030000000000000">
138<I>real<MATH CLASS="INLINE">
139-
140</MATH>identical<MATH CLASS="INLINE">
141-
142</MATH>points</I></A>
143</H4>
144<P><IMG WIDTH="504" HEIGHT="27" ALIGN="MIDDLE" BORDER="0"
145 SRC="img140.gif"
146 ALT="$\textstyle\parbox{\pboxargslen}{\em a b \/}$"> [<EM>MACRO</EM>]
147<BLOCKQUOTE>
148Return [ (A1<MATH CLASS="INLINE">
149-
150</MATH>B1)**2 + (A2<MATH CLASS="INLINE">
151-
152</MATH>B2)**2 ] in lisp (prefix) notation.
153The second value is the list of variables (A1 B1 A2 B2). Note that
154if the distance between two complex points A, B is zero, it does not
155mean that the points are identical. Use IDENTICAL<MATH CLASS="INLINE">
156-
157</MATH>POINTS to express
158the fact that A and B are really identical. Use this macro in
159conclusions of theorems, as it may not be possible to prove that A
160and B are trully identical in the complex domain.</BLOCKQUOTE><H4><A NAME="SECTION00080040000000000000">
161<I>identical<MATH CLASS="INLINE">
162-
163</MATH>points</I></A>
164</H4>
165<P><IMG WIDTH="504" HEIGHT="27" ALIGN="MIDDLE" BORDER="0"
166 SRC="img140.gif"
167 ALT="$\textstyle\parbox{\pboxargslen}{\em a b \/}$"> [<EM>MACRO</EM>]
168<BLOCKQUOTE>
169Return [ A1<MATH CLASS="INLINE">
170-
171</MATH>B1, A2<MATH CLASS="INLINE">
172-
173</MATH>B2 ] in lisp (prefix) notation.
174The second value is the list of variables (A1 B1 A2 B2). Note that
175sometimes one is able to prove only that (A1<MATH CLASS="INLINE">
176-
177</MATH>B1)**2 + (A2<MATH CLASS="INLINE">
178-
179</MATH>B2)**2
180= 0. This equation in the complex domain has solutions with A and B
181distinct. Use REAL<MATH CLASS="INLINE">
182-
183</MATH>IDENTICAL<MATH CLASS="INLINE">
184-
185</MATH>POINTS to express the fact that the
186distance between two points is 0. Use this macro in assumptions of
187theorems, although this is seldom necessary because we assume most of
188the time that in assumptions all points are distinct if they are
189denoted by different symbols. </BLOCKQUOTE><H4><A NAME="SECTION00080050000000000000">
190<I>perpendicular</I></A>
191</H4>
192<P><IMG WIDTH="562" HEIGHT="27" ALIGN="MIDDLE" BORDER="0"
193 SRC="img141.gif"
194 ALT="$\textstyle\parbox{\pboxargslen}{\em a b c d \/}$"> [<EM>MACRO</EM>]
195<BLOCKQUOTE>
196Return [ (A1<MATH CLASS="INLINE">
197-
198</MATH>B1) * (C1<MATH CLASS="INLINE">
199-
200</MATH>D1) + (A2<MATH CLASS="INLINE">
201-
202</MATH>B2) * (C2<MATH CLASS="INLINE">
203-
204</MATH>D2) ] in lisp
205(prefix) notation. The second value is the list of variables (A1 A2
206B1 B2 C1 C2 D1 D2). </BLOCKQUOTE><H4><A NAME="SECTION00080060000000000000">
207<I>parallel</I></A>
208</H4>
209<P><IMG WIDTH="562" HEIGHT="27" ALIGN="MIDDLE" BORDER="0"
210 SRC="img141.gif"
211 ALT="$\textstyle\parbox{\pboxargslen}{\em a b c d \/}$"> [<EM>MACRO</EM>]
212<BLOCKQUOTE>
213Return [ (A1<MATH CLASS="INLINE">
214-
215</MATH>B1) * (C2<MATH CLASS="INLINE">
216-
217</MATH>D2) <MATH CLASS="INLINE">
218-
219</MATH> (A2<MATH CLASS="INLINE">
220-
221</MATH>B2) * (C1<MATH CLASS="INLINE">
222-
223</MATH>D1) ] in lisp
224(prefix) notation. The second value is the list of variables (A1 A2
225B1 B2 C1 C2 D1 D2). </BLOCKQUOTE><H4><A NAME="SECTION00080070000000000000">
226<I>collinear</I></A>
227</H4>
228<P><IMG WIDTH="598" HEIGHT="27" ALIGN="MIDDLE" BORDER="0"
229 SRC="img142.gif"
230 ALT="$\textstyle\parbox{\pboxargslen}{\em a b c \/}$"> [<EM>MACRO</EM>]
231<BLOCKQUOTE>
232Return the determinant det([[A1,A2,1],[B1,B2,1],[C1,C2,1]]) in lisp
233(prefix) notation. The second value is the list of variables (A1 A2
234B1 B2 C1 C2). </BLOCKQUOTE><H4><A NAME="SECTION00080080000000000000">
235<I>equidistant</I></A>
236</H4>
237<P><IMG WIDTH="562" HEIGHT="27" ALIGN="MIDDLE" BORDER="0"
238 SRC="img141.gif"
239 ALT="$\textstyle\parbox{\pboxargslen}{\em a b c d \/}$"> [<EM>MACRO</EM>]
240<BLOCKQUOTE>
241Return the polynomial
242[(A1<MATH CLASS="INLINE">
243-
244</MATH>B1)**2+(A2<MATH CLASS="INLINE">
245-
246</MATH>B2)**2<MATH CLASS="INLINE">
247-
248</MATH>(C1<MATH CLASS="INLINE">
249-
250</MATH>D1)**2<MATH CLASS="INLINE">
251-
252</MATH>(C2<MATH CLASS="INLINE">
253-
254</MATH>D2)**2] in lisp
255(prefix) notation. The second value is the list of variables (A1 A2
256B1 B2 C1 C2 D1 D2). </BLOCKQUOTE><H4><A NAME="SECTION00080090000000000000">
257<I>euclidean<MATH CLASS="INLINE">
258-
259</MATH>distance</I></A>
260</H4>
261<P><IMG WIDTH="522" HEIGHT="27" ALIGN="MIDDLE" BORDER="0"
262 SRC="img143.gif"
263 ALT="$\textstyle\parbox{\pboxargslen}{\em a b r \/}$"> [<EM>MACRO</EM>]
264<BLOCKQUOTE>
265Return the polynomial [(A1<MATH CLASS="INLINE">
266-
267</MATH>B1)**2+(A2<MATH CLASS="INLINE">
268-
269</MATH>B2)**2<MATH CLASS="INLINE">
270-
271</MATH>R&#94;2] in
272lisp (prefix) notation. The second value is the list of variables (A1
273A2 B1 B2 R). </BLOCKQUOTE><H4><A NAME="SECTION000800100000000000000">
274<I>midpoint</I></A>
275</H4>
276<P><IMG WIDTH="598" HEIGHT="27" ALIGN="MIDDLE" BORDER="0"
277 SRC="img142.gif"
278 ALT="$\textstyle\parbox{\pboxargslen}{\em a b c \/}$"> [<EM>MACRO</EM>]
279<BLOCKQUOTE>
280Express the fact that C is a midpoint of the segment AB.
281Returns the list [ 2*C1<MATH CLASS="INLINE">
282-
283</MATH>A1<MATH CLASS="INLINE">
284-
285</MATH>B1, 2*C2<MATH CLASS="INLINE">
286-
287</MATH>A2<MATH CLASS="INLINE">
288-
289</MATH>B2 ]. The second value
290returned is the list of variables (A1 A2 B1 B2 C1 C2).</BLOCKQUOTE><H4><A NAME="SECTION000800110000000000000">
291<I>translate<MATH CLASS="INLINE">
292-
293</MATH>statements</I></A>
294</H4>
295<P><IMG WIDTH="507" HEIGHT="27" ALIGN="MIDDLE" BORDER="0"
296 SRC="img144.gif"
297 ALT="$\textstyle\parbox{\pboxargslen}{\em {\sf \&rest} statements \/}$"> [<EM>MACRO</EM>]
298<BLOCKQUOTE>
299 </BLOCKQUOTE><H4><A NAME="SECTION000800120000000000000">
300<I>translate<MATH CLASS="INLINE">
301-
302</MATH>assumptions</I></A>
303</H4>
304<P><IMG WIDTH="498" HEIGHT="29" ALIGN="MIDDLE" BORDER="0"
305 SRC="img145.gif"
306 ALT="$\textstyle\parbox{\pboxargslen}{\em {\sf \&rest} assumptions \/}$"> [<EM>MACRO</EM>]
307<BLOCKQUOTE>
308 </BLOCKQUOTE><H4><A NAME="SECTION000800130000000000000">
309<I>translate<MATH CLASS="INLINE">
310-
311</MATH>conclusions</I></A>
312</H4>
313<P><IMG WIDTH="504" HEIGHT="27" ALIGN="MIDDLE" BORDER="0"
314 SRC="img146.gif"
315 ALT="$\textstyle\parbox{\pboxargslen}{\em {\sf \&rest} conclusions \/}$"> [<EM>MACRO</EM>]
316<BLOCKQUOTE>
317 </BLOCKQUOTE><H4><A NAME="SECTION000800140000000000000">
318<I>translate<MATH CLASS="INLINE">
319-
320</MATH>theorem</I></A>
321</H4>
322<P><IMG WIDTH="526" HEIGHT="31" ALIGN="MIDDLE" BORDER="0"
323 SRC="img147.gif"
324 ALT="$\textstyle\parbox{\pboxargslen}{\em ({\sf \&rest} assumptions) ({\sf \&rest} conclusions) \/}$"> [<EM>MACRO</EM>]
325<BLOCKQUOTE>
326Translates a planar geometry theorem into a system of polynomial
327equations. Each assumption or conclusion takes form of a declaration
328(RELATION<MATH CLASS="INLINE">
329-
330</MATH>NAME A B C ...) where A B C are points, entered as
331symbols and RELATION<MATH CLASS="INLINE">
332-
333</MATH>NAME is a name of a geometric relation, for
334example, (COLLINEAR A B C) means that points A, B, C are all
335collinear. The translated equations use the convention that (A1,A2)
336are the coordinates of the point A. This macro returns multiple
337values. The first value is a list of polynomial expressions and the
338second value is an automatically generated list of variables from
339points A, B, C, etc. For convenience, several macros have been
340defined in order to make specifying common geometric relations easy. </BLOCKQUOTE><H4><A NAME="SECTION000800150000000000000">
341<I>prove<MATH CLASS="INLINE">
342-
343</MATH>theorem</I></A>
344</H4>
345<P><IMG WIDTH="549" HEIGHT="31" ALIGN="MIDDLE" BORDER="0"
346 SRC="img148.gif"
347 ALT="$\textstyle\parbox{\pboxargslen}{\em ({\sf \&rest} assumptions) ({\sf \&rest}
348 conclusions) {\sf \&key} (order
349 *prover$-$order*) \/}$"> [<EM>MACRO</EM>]
350<BLOCKQUOTE>
351Proves a geometric theorem, specified in the same manner as in
352the macro TRANSLATE<MATH CLASS="INLINE">
353-
354</MATH>THEOREM. The proof is achieved by a call to
355IDEAL<MATH CLASS="INLINE">
356-
357</MATH>POLYSATURATION. The theorem is true if the returned value
358is a trivial ideal containing 1.</BLOCKQUOTE><HR>
359<!--Navigation Panel-->
360<A NAME="tex2html989"
361 HREF="node9.html">
362<IMG WIDTH="37" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="next" SRC="next_motif.gif"></A>
363<A NAME="tex2html986"
364 HREF="manual.html">
365<IMG WIDTH="26" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="up" SRC="up_motif.gif"></A>
366<A NAME="tex2html980"
367 HREF="node7.html">
368<IMG WIDTH="63" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="previous" SRC="previous_motif.gif"></A>
369<A NAME="tex2html988"
370 HREF="node1.html">
371<IMG WIDTH="65" HEIGHT="24" ALIGN="BOTTOM" BORDER="0" ALT="contents" SRC="contents_motif.gif"></A>
372<BR>
373<B> Next:</B> <A NAME="tex2html990"
374 HREF="node9.html">The Monomial Order Package</A>
375<B> Up:</B> <A NAME="tex2html987"
376 HREF="manual.html">CGBLisp User Guide and</A>
377<B> Previous:</B> <A NAME="tex2html981"
378 HREF="node7.html">The Dynamical Systems package</A>
379<!--End of Navigation Panel-->
380<ADDRESS>
381<I>Marek Rychlik</I>
382<BR><I>3/21/1998</I>
383</ADDRESS>
384</BODY>
385</HTML>
Note: See TracBrowser for help on using the repository browser.