A study of the 1984 report An Automatic Proof Procedure For Several Geometries by Th. Bruyn and H.L. Claasen
T.T. Bruyn (TU Delft - Electrical Engineering, Mathematics and Computer Science)
JMAM Van Neerven – Mentor
B. van den Dries – Graduation committee member
Klaas Pieter Hart – Graduation committee member
JFM Tonino – Graduation committee member
More Info
expand_more
Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.
Abstract
This report is a discussion of the 1984 report 'An automatic proof procedure for several geometries' by Th. Bruyn and H.L. Claasen, inspired by a personal desire to understand the work of Th. Bruyn. See: http://resolver.tudelft.nl/uuid:b768c6ce-f625-4236-9b0b-32a47fab143e
Bruyn and Claasen prove that certain true propositions of the theory of intersections within the two-dimensional projective geometry over the real numbers can be formulated by use of figures. It is proven that figures obtained by manipulating these figures will also correspond to propositions. The method to do so proves that the obtained propositions are a direct consequence of the original propositions and are therefore proven to be true. One of their main results is to use the theorem of Pappus to generate the theorem of Desargues, thereby proving that Desargues follows from Pappus (something that is well known in projective geometry).
This report aims to give a comprehensive explanation of their method as well as a detailed demonstration of their procedure. It is a summary of their work with added explanations and examples.