# A study of the 1984 report An Automatic Proof Procedure For Several Geometries by Th. Bruyn and H.L. Claasen

A study of the 1984 report An Automatic Proof Procedure For Several Geometries by Th. Bruyn and H.L. Claasen

AuthorBruyn, Tim (TU Delft Electrical Engineering, Mathematics and Computer Science; TU Delft Delft Institute of Applied Mathematics)

van Neerven, Jan (mentor)

van den Dries, Bart (graduation committee)

Hart, Klaas Pieter (graduation committee)

Tonino, Hans (graduation committee)

Delft University of Technology

Date2017-08-23

AbstractThis 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.

Subject To reference this document use:http://resolver.tudelft.nl/uuid:53cc492f-1fd0-4b0e-a879-286f54258904

Part of collectionStudent theses

Document typebachelor thesis