[1] | 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">
|
---|
| 116 | The 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>
|
---|
| 127 | Admissible 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>
|
---|
| 134 | Return symbol whose name is a concatenation of (SYMBOL<MATH CLASS="INLINE">
|
---|
| 135 | -
|
---|
| 136 | </MATH>NAME SYMBOL)
|
---|
| 137 | and 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>
|
---|
| 148 | Return [ (A1<MATH CLASS="INLINE">
|
---|
| 149 | -
|
---|
| 150 | </MATH>B1)**2 + (A2<MATH CLASS="INLINE">
|
---|
| 151 | -
|
---|
| 152 | </MATH>B2)**2 ] in lisp (prefix) notation.
|
---|
| 153 | The second value is the list of variables (A1 B1 A2 B2). Note that
|
---|
| 154 | if the distance between two complex points A, B is zero, it does not
|
---|
| 155 | mean that the points are identical. Use IDENTICAL<MATH CLASS="INLINE">
|
---|
| 156 | -
|
---|
| 157 | </MATH>POINTS to express
|
---|
| 158 | the fact that A and B are really identical. Use this macro in
|
---|
| 159 | conclusions of theorems, as it may not be possible to prove that A
|
---|
| 160 | and 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>
|
---|
| 169 | Return [ A1<MATH CLASS="INLINE">
|
---|
| 170 | -
|
---|
| 171 | </MATH>B1, A2<MATH CLASS="INLINE">
|
---|
| 172 | -
|
---|
| 173 | </MATH>B2 ] in lisp (prefix) notation.
|
---|
| 174 | The second value is the list of variables (A1 B1 A2 B2). Note that
|
---|
| 175 | sometimes 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
|
---|
| 181 | distinct. Use REAL<MATH CLASS="INLINE">
|
---|
| 182 | -
|
---|
| 183 | </MATH>IDENTICAL<MATH CLASS="INLINE">
|
---|
| 184 | -
|
---|
| 185 | </MATH>POINTS to express the fact that the
|
---|
| 186 | distance between two points is 0. Use this macro in assumptions of
|
---|
| 187 | theorems, although this is seldom necessary because we assume most of
|
---|
| 188 | the time that in assumptions all points are distinct if they are
|
---|
| 189 | denoted 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>
|
---|
| 196 | Return [ (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
|
---|
| 206 | B1 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>
|
---|
| 213 | Return [ (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
|
---|
| 225 | B1 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>
|
---|
| 232 | Return 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
|
---|
| 234 | B1 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>
|
---|
| 241 | Return 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
|
---|
| 256 | B1 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>
|
---|
| 265 | Return 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^2] in
|
---|
| 272 | lisp (prefix) notation. The second value is the list of variables (A1
|
---|
| 273 | A2 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>
|
---|
| 280 | Express the fact that C is a midpoint of the segment AB.
|
---|
| 281 | Returns 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
|
---|
| 290 | returned 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>
|
---|
| 326 | Translates a planar geometry theorem into a system of polynomial
|
---|
| 327 | equations. 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
|
---|
| 331 | symbols and RELATION<MATH CLASS="INLINE">
|
---|
| 332 | -
|
---|
| 333 | </MATH>NAME is a name of a geometric relation, for
|
---|
| 334 | example, (COLLINEAR A B C) means that points A, B, C are all
|
---|
| 335 | collinear. The translated equations use the convention that (A1,A2)
|
---|
| 336 | are the coordinates of the point A. This macro returns multiple
|
---|
| 337 | values. The first value is a list of polynomial expressions and the
|
---|
| 338 | second value is an automatically generated list of variables from
|
---|
| 339 | points A, B, C, etc. For convenience, several macros have been
|
---|
| 340 | defined 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>
|
---|
| 351 | Proves a geometric theorem, specified in the same manner as in
|
---|
| 352 | the macro TRANSLATE<MATH CLASS="INLINE">
|
---|
| 353 | -
|
---|
| 354 | </MATH>THEOREM. The proof is achieved by a call to
|
---|
| 355 | IDEAL<MATH CLASS="INLINE">
|
---|
| 356 | -
|
---|
| 357 | </MATH>POLYSATURATION. The theorem is true if the returned value
|
---|
| 358 | is 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>
|
---|