Edinburgh Research Explorer

Computer-Assisted Theorem Proving in Synthetic Geometry

Research output: Chapter in Book/Report/Conference proceedingChapter (peer-reviewed)

Original languageEnglish
Title of host publicationHandbook of Geometric Constraint Systems Principles
Place of PublicationNew York, USA
PublisherChapman and Hall/CRC
Chapter2
Pages21-60
Number of pages39
Edition1st
ISBN (Electronic)9781498738927
ISBN (Print)9781498738910
Publication statusPublished - 1 Aug 2018

Abstract

Computer-assisted proof in mathematics has been underway since the pioneering times of computers in the 1950s. Starting from early systems with very limited capability, Computer-Assisted Theorem Proving has evolved to demonstrate theorems never proved before by humans [156] and assist with monumental efforts spanning several man-years [116]. In this endeavour, geometry plays an important part, just as it has throughout the history of mathematics. This is due to its pervasive role: it is a paradigmatic form of reasoning, with applications to education, mathematical and physical research, but also to many applied areas such as robotics, computer vision, and CAD [48]. Moreover, many of the search techniques and other algorithmic features developed for geometric reasoning have influenced other areas of artificial intelligence.

ID: 74942355