-
Notifications
You must be signed in to change notification settings - Fork 23
Expand file tree
/
Copy pathautomated_theorem_prover.html
More file actions
175 lines (143 loc) · 10.4 KB
/
automated_theorem_prover.html
File metadata and controls
175 lines (143 loc) · 10.4 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html><head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<script type="text/javascript">
var tiki_cookie_jar = new Array();
tiki_cookie_jar = {
};
</script>
<script type="text/javascript" src="lib/tiki-js.js"></script><title>JGEX Documentation : An Automated Theorem Prover </title>
<link rel="StyleSheet" href="lib/1.css" type="text/css">
<link rel="StyleSheet" href="styles/cindydoc.css" type="text/css">
<link rel="alternate" type="application/xml" title="RSS Wiki" >
<style type="text/css">
<!--
.STYLE10 {font-size: 12px}
.STYLE12 { font-size: 16px;
font-weight: bold;
}
.STYLE3 {font-family: Verdana, Arial, Helvetica, sans-serif}
.style2 {font-size: 18px}
-->
</style>
</head>
<body>
<div id="overDiv" style="position: absolute; visibility: hidden; z-index: 1000;"></div>
<script type="text/javascript" language="JavaScript" src="lib/overlib.js"></script>
<div id="tiki-clean">
<div id="tiki-mid">
<div class="wikitopline">
<table><tbody><tr>
<td style="vertical-align: top;">
</td>
</tr></tbody></table>
</div>
<div class="wikitext">
<h2>An Automated Theorem Prover </h2>
<p><span class="STYLE12">1. Geometric and Non-Geometric Drawing</span></p>
<p><br />
In JGEX, The diagram generated by it is
geometric. At the right beginning of developing the drawing part of JGEX, we have kept the
proving and reasoning as our final goal since we treat geometric elements, such as points, lines,
and circles symbolically. Then we can apply the reasoning methods developed for over a quarter
of a century to proving and/or discovering properties of a geometric diagram constructed. We call
this kind of drawing Geometric Drawing.</p>
<p><br />
For a diagram generated by JGEX, we keep a set of algebraic equations of the geometry constraints,
so that we can prove or disprove properties of it with our algebraic methods efficiently. Especially,
with Geometric Drawing, all nondegenerate conditions can be generated automatically.</p>
<p class="STYLE12">2. Use of Algebraic Equations</p>
<p>A geometrical constraint in the hypotheses can be represent as one or two polynomial equalities on
the coordinates of points. For example, for predicate that A, B, C are collinear, the corresponding
polynomial equation is: <img src="effects/e1.gif" width="325" height="23" />. In this way, the hypotheses can
be expressed as a set of polynomial equations: </p>
<p><img src="effects/equation1.gif" width="400" height="130" /><br />
The next step is to triangulate 3 the polynomial set so that each polynomial introduces only one
new (dependent) variable xi. Thus the polynomial set is transformed to triangular form: </p>
<p><img src="effects/equation2.gif" width="400" height="130" /><br />
The variables <span class="STYLE3">u1, . . . , ud</span> can be arbitrarily chosen and once they are fixed, the variables <span class="STYLE3">x1, . . . , xr</span> can be successively solved. When one or two of variables <span class="STYLE3">u1, . . . , ud</span> are changed with the mouse,
then the variables of <span class="STYLE3">x1, . . . , xr</span> are updated to achieve the dynamic geometry effects. </p>
<p><br />
One of advantages of this approach to drawing is that the reasoning with algebraic methods can
be immediately applied to the diagram. Currently, we have implemented Wu’s method in JGEX
and the Gr¨obner basis methods for various formulations (see [4]) are under implementing. Many<br />
important and subtle geometry issues are closed related to Wu’s method which are impossible to
discuss without the underlying theory of Wu’s method.
Another important advantage of use of polynomials is that we can construct all diagrams or cases
with the leading degree in <span class="style2">x</span><span class="STYLE10">j </span>≤ 4, since JGEX implements the formulas for quadratic, cubic, and
quartic equations. </p>
<p align="left"><span class="STYLE12">3. Elimination of Duplicated Points </span><br />
As a direct application of the JGEX algebraic proof engine, we can eliminate a newly constructed
point if it is identical to one of the previously constructed points. The three commercial systems
can only eliminate this point numerically. Since drawing a geometry diagram is so easy with a few
mouse clicks, we repeatedly observed this phenomenon at the early stage of developing JGEX. </p>
<p align="left">Example. Let ABC be an isosceles triangle with AB = AC.
Reflecting AB with respect to (wrpt) BC, we get segment BA';
then reflecting AC wrpt BC, we get segment CA''. Points A'
and A'' are actually identical. </p>
<p align="left"><br />
This is a simple example, but we have also encountered cases in
which the identity itself is a relatively deep theorem. Here is our
approach. Whenever a new point is constructed, we first check
whether this point is identical to a previous one numerically. If
so, we use Wu’s method to check the identity. If the identity is
valid, we eliminate this point. Without the powerful algebraic
proof engine, it could eliminate the redundant points with only approximate
numerical computations. But approximate
numerical computations does not prove points A and
X to be identical. </p>
<h5 align="left" class="STYLE12"><br />
4. Automated Generation of Nondegenerate conditions </h5>
<p align="left"><br />
A geometry theorem is true generally under some additional conditions called nondegenerate
conditions. The identification of nondegenerate conditions is subtle.<br />
<br />
<strong>Figure 2: One Form of the Nine-Point Circle Theorem</strong><br />
<span class="STYLE3">Example 1. (One form of the nine-point circle theorem) Let points D, E and F be the three feet
of the altitudes of triangle ABC. Let N be such that NF = NE and NF = ND, and M be the
midpoint of AB. Then NM = NF. </span> </p>
<p align="center"><img src="effects/9pt.gif" width="468" height="225" border="1" /><br />
For this example, beside the condition that A, B and C are not collinear, we need at least the
nondegenerate condition that triangle ABC is not a right triangle, a subtle condition which is
not easy to detect. However, with geometric drawing and the reasoning ability of JGEX, we can
generate the nondegenerate conditions for a class of geometry statements of the constructive type. </p>
<p align="left"><br />
The existence of point N implies the nondegenerate condition that points D, E, F are not collinear.
Since points D, E, F are fixed points, we need to generate nondegenerate conditions that only
contains free points. This is not an easy work, however, we can generate the polynomial equations<br />
for this nondegenerate condition and check if the hypotheses are consistent or not with Wu’s method.
This is very useful for a theorem to be complete. For most of the theorems we encountered, the
nondegenerate conditions with geometric meanings can be generated automatically and thus we
can give a complete description of the geometry statements. </p>
<h3><br>
</h3>
<h4 class="STYLE12">5.
The Six Different Methods </h4>
<p class="wikitext">Java Geometry Expert (<strong>JGEX</strong>) is a powerful computer program for geometric reasoning. Within its domain, it invites comparison with the best of human geometry provers. It implements most of the effective methods for geometric reasoning introduced in the past twenty years. JGEX also implements the the following methods. ( <strong>Note</strong>: in this beta version, the area method and vector method is under developing). </p>
<p class="wikitext"><br />
<strong>1. <a href="wu.html">Wu's method</a></strong> is the most powerful method in terms of proving difficult geometry theorems. Wu's method is a coordinate-based method. It first transfers geometry conditions into poiynomial equations in the coordinates of the points involved, then deals with the polynomial equations with the characteristic set method. </p>
<p class="wikitext"><strong>2. <a href="groebner.html">The Groebner basis method</a></strong> is also a coordinate-based method. Instead of using the characteristic set method, it uses the Grobner basis method to deal with the polynomial equations.</p>
<p class="wikitext"><br />
<strong>3. <a href="area.html">The area method</a></strong> uses high-level geometric lemmas about geometry invariants such as the area and the Pythagorean difference as the basic tool of proving geometry theorems. The method has been used to produce short, elegant, and human- readable proofs for more than 500 geometry theorems. </p>
<p class="wikitext"><strong>4. <a href="full_angle_method.html">The full-angle method</a></strong> is based on the calculation of full-angles. Full-angle method is not a decision procedure. But this method also has its advantages: all the proofs produced by the method are very short, and it has been used to prove several theorems that all the other methods fail to prove because of very large polynomials occurring in the proving process. </p>
<p class="wikitext">5. <a href="deductive_database.html"><strong>The Deductive Database Method</strong></a> based on Full-Angle. <br />
<br />
<strong>6. Vector method</strong> This method is a variant of the area method and is based on the calculation of vectors and complex numbers.</p>
<p class="wikitext"><br />
<br />
To use more than one method in the prover, we can produce a variety of proofs with different styles. This might be important in using JGEX to geometry education, since different methods allow students to explore different and better proofs. </p>
<h5 class="STYLE12"> </h5>
<h5 class="STYLE12">6. The Prove Pane</h5>
<p align="left"><img src="images2/ppane.gif" width="344" height="395" border="1" /></p>
<p align="left">The prove pane is on the left of the JGEX main window. It has a toolbar on the top and a tabbed pane on the bottom.</p>
<p align="left"> </p>
<p align="left"><strong>See Also:</strong></p>
<ul><li><a href="Nine_Point_Circle.html">The Nine Point Circle Theorem</a></li>
</ul>
<p align="left"> <br>
<tt> </tt></p>
</div>
<p class="editdate">JGEX Help </p>
</div>
</div>
</body></html>