Visual Reasoning in Geometry Theorem Proving

1 Introduction

The question of visual imagery in humans has been a controversial subject within cognitive psychology [Anderson, 1979, Kosslyn, 1980, Shepard and Cooper, 1982, Pylyshyn, 1973]. No one doubts the conscious phenomena of imagery, or the act of visualization. What is problematic is the ultimate nature of images as mental representation [Johnson-Laird, 1983]. Is there a single underlying form of mental representation and are images only epiphenominal; or are images a distinct sort of mental representation? Regardless of the out­ come of this debate, that visual imagery as a natural means of dealing with spatial problems will remain irrefutable.

Visual imagery, or visual reasoning, as a useful tool for scientists and mathematicians has been demon­ strated in the past [McKim, I 980, Kosslyn, 1983, Simon, I 987]. Our goal is to explore visual reasoning as a computationally feasible tool in problem solving. We investigate its role in the classical AI domain, dis­ covering proofs for theorems in euclidean plane geom­ etry. To discover a proof requires ingenuity, imagination, and insights to a problem. Considering a model of the problem generally provides most valuable insights to a problem. In our domain, the model is a diagram, and through its manipulation the problem starts unfolding. I Jeuristic values of a model, or a dia­ gram, are that it provides a counter-example of an unprovable theorem and more importantly that it serves as a vehicle for "perceptual reasoning," perceptual in the sense that many facts are self-evident from the diagram and that they need not be established from fundamental ax10ms.

Building theorem-proving systems for geometry has been attempted frequently in the past [Gelernter, 1958, Gclcrnter, 1963, Goldstein, 1973, Nevins, 1974, Anderson, 1981, Anderson, 1983, Anderson, 1985, Coelho and Pereira, 1986, Lakin and Simon, 1987]. See [Coelho and Pereira, 1986] for a comparative study of previous work. Most notable system among them is the Geometry Theorem Prover [Gelernter, 1958, Gelcrnter, 1963], which was one of the earliest auto­ mated theorem provers and was distinguished by its re­ liance on a diagram to guide the proof. The prover used the diagram as the pruning heuristic, e.g., it rejected as false any goal that was not true in the diagram. Its use of diagrams, however, was limited in that diagrams supplied only yes or no answers to questions of the form: "Is segment AB equal to Segment CD in the fig­ ure?" Note that finite precision arithmetic, applied to the diagram, occasionally caused a provable sub-goal to be pruned erroneously. Purthermore, constructions such as adding lines to the diagram were done only as the last resource, and the help lines were drawn by randomly connecting any unconnected points, when all else failed .

Our aim is to further explore the heuristic values of the diagram, and show a method that allows the dia­ grams to be percd11ed, or seen, and to be manipulated in a creative manner, similar to what may occur in hu­ man visual reasoning. To represent geometric features, we usc an algebraic notation and capture what may be the key computational efficiencies that occur in human visual reasoning.

In the next section visual reasoning in plane geometry is discussed . In Section 3, a representation scheme by which geometric features arc described is given. In Section 4, some useful patterns that are found in many geometry problems are identified and the methods by which they may be recognized are discussed . In Section 5, we describe Machine's I, an early version of machine implementation, which may be used as a front-end heuristic device to a more general geometry theorem prover. Finally conclusions appear in Section 6.

2 Visual Reasoning in Geometry

Visual reasoning in geometry may be considered as a two-step process: patterning, and analysis. Patterning, or pattern-seeking, as an active nature of visual percep­ tion has been formulated as a theory, known as Gestalt theory, by psychologists [McKim, 1980]. The pattern that we perceive in a problem strongly influences the manner by which we approach the problem. So pow­ erful is the perceptual tendency to perceive meaningful patterns, we will fill in missing parts. This effect is known as closure. Seeking meaningful patterns or gen­ erating them, or closing-in, is a particularly effective aid in geometry theorem proving. Once a meaningful pat­ tern is found, its implications are analyzed, or inferred.

Consider the problem in Figure 1: "Given a square (ABCD), take the midpoints of the four sides, and prove that the two triangles (EF/f) and (GF/f) are congruent to each other."

To solve this problem, backward-chaining methods used by most of previous geometry-theorem proving systems [Gelernter, 1963, Goldstein, 1973, Coelho and Pereira, 1986] would first set up a goal to prove that the two triangles are congruent, then set up sub-goals to prove that their corresponding sides are congruent, and then set up more sub-goals, repeatedly, to show that each pair of corresponding sides are congruent, and so on. A human mathematician, given the problem, may perceive an apparent symmetry in the diagram by ob­ serving a reflection across (Fif) or across (EG). As a symmetry is observed, it can be shown with littl~ effort that the two triangles are congruent, and thus repeated proofs can be avoided.

Consider another problem as shown in Figure 2: "Prove that the midpoint of the hypotenuse of a right triangle is equidistant from the three vertices." To solve this problem, suppose the right triangle (A /JC) is half­ turned, or turned by 180 degrees, about the midpoint. This half-turn generates (DCB), which is a copy of (ABC) 180 degree turned about (M). The two triangles form a rectangle (ABCD) . Once a rectangle is seen and its diagonals are computed, it can be trivially inferred that the two diagonals are congruent and that they bisect one another, and thus, the four line segments are congruent, and so on.

Observe that we have obtained an outline, or a plan, for a proof by finding a line symmetry in Figure l . We have obtained useful infonnation for a proof in I 'igurc 2 by turning the right triangle and transforming it to a rectangle. We show in the next section a nota­ tion that can capture important heuristics for proving geometry theorems. The notation can suggest that there is a reflection in one problem, and that a half-tum maybe useful in another.

3 Representing Geometric Features

A good choice of representation can greatly facilitate the recognition task. Suppose we represent the square in Figure I, using the primitives a= j and b = -+ , by the string (a(f)b) · (b(f)a), where (f) is to join a pair of primitives, and · to describe a closed object (Definitions follow below) . This string is a palindrome. As we shall sec later, a palindrome strongly suggests that there is some type of symmetry. It is this capacity that we are after. The representation is simple. It is also syntactic, and thus geometric features can be manipulated easily and systematically. More importantly, this method to pattern seeking provides useful semantic information despite its syntactic appearance.

3.1 Shape Primitives and their Operations

We define shape primitives as directional pairs (p.l, p .a) , where p is the name of the primitive, p .l is the length, p .a is the angle. The angle increases in the counter-clock wise direction, 0 :::;; p .a < 180, thus allow­ ing a unique representation of a primitive.

Shape primitives are connected to form and charac­ terize a structural pattern. We first define simp!ejoining operations as shown in Figure 3. We show three ways of joining a pair of primitives, such that each of the primitives has two distinct connection points, a head and a tail. These three binary operations, denoted by ®, G , ®,allow a primitive to be attached to the other primitive only at its head or tail. G and ® operations arc commutative, while ® is not. Similar techniques have been used in the past in the pattern recognition research in computer vi sion [Shaw, 1972].

Operation + creates a primitive out of two joined primitives. In Figure 4, +(a~b) constructs primitive c, +(a9b) constructs d, and +(a®h) constructs d'. As a short hand notation, where there is no confusion, we will write a+ b to mean any of these three constructions.

Operation · is to describe a closed structure. For example the three triangles in Figure 4 can be described by c·(a$b), b·(a$d), and (d'$a)·h, from left to right. We let operation · be commutative. Although we have defined three join operations above, we may only use operation $ and operation · to describe a tri­ angle. This is to guarantee a unique representation from which other equivalent representations can be com­ puted.

The structural joining operation, denoted by .IN( a), joins a pair of closed structures over primitive a . .IN( a) is a useful operator in describing a non-convex struc­ ture. Thus, the non-convex quadrilateral in Figure 5 may be expressed as ((c$e) · d) .IN( c) ((c$./) · g), or simply (ced) .IN(c) (cfg), where (p1 .. .pn) denotes an n­ sided polygon and P; s are its primitives. Operation .! N is also commutative.

Most of geometric objects can now be represented using our shape primitives and their operations shown above. Note that the starting point may be added in the definition of a primitive, or a rule may be defmcd that connects two disjoint primitives, etc., thus making the method more general. This extension can be made in a straightforward manner, and in this paper we have adopted a simplifying notation for a simpler discussion. In the next section we discuss visual reasoning, or pat­ tern seeking, using our representation.

4 Patterning and Reasoning

Geometric objects provide interesting abstractions of many patterns we fmd in nature, art, and industry. Synunetry and dilations, or scaling, are among them. Finding a line of symmetry or a point of symmetry provides important clues in the search of a proof. Where there is no apparent symmetry, it almost always pays to create one. As symmetry is to congruence, dilations is to similarity. A good many geometry problems like so many objects around us contain dilations. Identifying a dilation when it is present or by filling in missing parts when it is not apparent is as effective as finding symmetry.

Observe that it is necessary to recognize or generate meaningful patterns in a systematic manner. We may interpret each shape primitive as a symbol permissible in some grammar, then, the syntactic pattern recogni­ tion process is a straightforward task. In this report, we do not establish a formal grammar, but provide an in­ formal description of the recognition process and show simple examples. For definitions of the patterns that we discuss below, and for more examples of using such patterns to guide the search of a proof, sec [Kim, 1988].

4.1 Finding a Point Symmetry

Consider the parallelogram (a$b) · (b$a) in Figure 6. Syntactically, its string representation is a palindrome. A palindrome:

suggests that there is a point symmetry in the structure. A palindrome uniquely defines a structure with a point symmetry and that a structure with a point symmetry may be uniquely defined as a palindrome.

As an example, we show below a series of inferencing processes that may occur given a palindrome ( a(]Jh) · (b$a) , where a is not perpendicular to b: (I) the structure is a parallelogram, (2) its diagonals c and d are computed, c is constructed from +(a9b) and d from +(a~ b), (3) the diagonals of a parallelogram bisect one another, ( 4) but c.l-=1= d.!, hence the structure is not a rectangle, ( 5) and thus, our symmetry is only a point symmetry not a line symmetry, (6) the point of sym­ metry is the intersection of the two diagonals c and d, and so on.

4.2 Finding a Line Symmetry (Reflection)

Informally, a reflection is a mirror image provided by an axis of symmetry. Without loosing generality, a re­ flection may be thought of as having two congruent structures joined over the axis.

Let w be a string representation that describes an isosceles triangle, a · (bEjjc) , where two of the three primitives are of equal length. Then w contains a re­ flection and its axis can be computed in a straightfor­ ward manner.

Consider the quadrilateral in Figure 7 (a$b)·(a'Ejjb'), a'.l=a.l, b'.l=b.l. Let c' be a+a'. Triangle a(jjc' · a' is an isosceles triangle and its axis is d = a+ c, where c is defined by: c.a = c' .a , c.!= c' .1/2, c' = (c(jjc) . Then (acd) is a reflection of (a'cd) over d. Similarly, c'Ejjb' · b is an isosceles triangle and its axis e can be computed in a straightforward manner. The quadrilateral contains a reflection in line (dEt>e), over which (abde) and (a'b'de) are joined.

4.3 .Finding a Dilation (Scalin~)

In Figure 8, the triangle (aE!Ja) · (c$(b$b)) contains a scaled triangle:

A string representation which is of the form w · w' , where w or w' contains ( ... E!)a(jja(jj .. . E!)bE!)b) , or w is of the form ( ... Ejja(j)a) and w' of the form ( .. . E!)bEt>b) , where a and b arc two distinct primitives, suggest that there is a dilation in the structure and that the point of dilation is where the two primitives meet.

Having discussed the principles of finding useful pat­ terns using our representation, we show an example below, and provide a summary of what may occur in solving the problem. For more examples, see [Kim, 1988].

4.4 An Example

The power of imagery becomes obvious with more in­ volved problems. Consider the perpendicular bisector concurrence theorem depicted in Figure 9.

The theorem states that the perpendicular bisectors of the sides of a triangle are concurrent and that their point of concurrency is equidistant from the vertices of the triangle. We let (AB) denote a line segment connecting two points (A) and (B) . We assume that the problem is given using this notation. In the figure (DM) and (EM) are two bisectors with the point of concurrency (M) . I laving shown that the three line segments (AM), (BM), and (CM) arc congruent by showing two re­ flections, the proof is complete if (FM) is shown to be the third bisector. We let (ABC) be x · (z$y), describ­ ing (AJJ), (JJC), and (A C) by x , y, and z, respectively, and let a.!= x.l/2 and b.!= y.l/2 . We, then construct d and e such that d is the perpendicular bisector of (aEt>a) and e is the perpendicular bisector of (bEt>b) . As the two intersecting perpendicular bisectors have been defined it follows that:

(gda) RL(d) (dah) ,

where RL( d) denotes a reflection over d. Thus g.!= h.!. Similarly, h. I= i.l. Thus g.!= h. I= i .l. Following our definition of reflection, (zEBz) · g, i.l =g.!, contains a reflection in line f such that f = +( cG g), and it follows that fis the perpendicular bisector of (A C).

5 An Implementation: Machine ' s I

"Machine's I (for eye)" is a rule-based program that has been implemented in ECLPS [IBM Enhanced Com­ mon Lisp Production System, IBM, 1988], as a front­ end heuristic device to a geometry theorem prover. A user presents a problem to Machine's I by declaring the premises and the goal. The program then builds a model, or a diagram, of the problem, draws it, and de­ scribes it in terms of shape primitives and the oper­ ations. Shape primitives and structures have been represented by working memory elements, and their manipulations have been implemented as ECLPS rules.

The program first starts to pattern: Obvious patterns are detected, or a meaningful pattern is created. Note that in patterning, not only the premises but the goal may provide a useful clue. As patterning progresses, new facts are inferred. In fact, this patterning phase may be considered as a mixture of backward and for­ ward chaining. Backward in the sense that the goal to prove may strongly influences the patterning, and for­ ward by the way reasoning proceeds from the premises. Having patterned, the results may be passed to a ge­ ometry theorem prover, so that a proof can be com­ pleted. It has been observed that for simple theorems the proof was often immediate after the patterning phase.

Much of the proof procedures addressed in this paper can be efficiently implemented in ECLPS due to its power. Unlike most resolution-based mechanical the­ orem proving systems in Prolog that lack operational semantics [Coelho and Pereira, 1986], ECLPS provides powerful demand-driven pattern matching capabiUties [Schor et al., 1986], which allow a dynamic pattern matching. More, it provides a flexible control strategy by prioritizing rule firings .

6 Conclusions

We have shown that a simple syntactic method pro­ vided powerful heuristic information for proving geom­ etry theorems. The representation is simple, easy to manipulate, and yet it captures what may be the key computational efficiencies that occur in human visual reasoning. We do not have a good characterization of what is involved in human visual reasoning. Nonethe­ less, the impUcations of capturing visual heuristics in a simple notation are great and need to be pursued fur­ ther.

Acknowledgements

The author is indebted to D. Sabbah and S. Addanki for their many valuable suggestions, H. Lee for his help in ECLPS, C. Alberga and D. Ferguson for their help­ ful comments on the draft. Special thanks are also due to S. Kosslyn for a stimulating initial discussion, and the contents of the manuscript has been greatly im­ proved by the comments of A Newell.