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

Bachelor thesis (2017)

Authors

T.T. Bruyn Electrical Engineering, Mathematics and Computer Science

Contributors

B. van den Dries (graduation committee member)
K.P. Hart (graduation committee member)
J.F.M. Tonino (graduation committee member)
Faculty
Electrical Engineering, Mathematics and Computer Science, Electrical Engineering, Mathematics and Computer Science
Copyright: © 2017 Tim Bruyn
More Info
expand_more

Published Date

23-08-2017

Language

English

Reuse Rights

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.

Faculty

Electrical Engineering, Mathematics and Computer Science

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.