Checking the Correctness of Theorems in Geometry

of radicals using rationals, unication. Abstract. Constraint Logic Programming can be advantageously used to deal with quadratic constraints stemming from the verication of planar geometry theorems. A hybrid symbolic{ numeric representation involving radicals and multiple precision rationals is used to denote the results of quadratic equations. A unication{like algorithm tests for the equality of two expres-sions using that representation. The proposed approach also utilizes geometric transformations to reduce the number of quadratic equations dening geometric constructions involving circles and straight lines. A large number (512) of geometry theorems has been veried using the proposed approach. Those theorems had been proven correct using a signicant more complex (exponential) approach in a treatise authored by Chou in 1988. Even though the proposed approach is based on verication-rather than strict correctness utilized by Chou- the eÆciency attained is polyno-mial thus making the approach useful in classroom situations where a construction attempted by student has to be quickly validated or refuted. 1