Please use this identifier to cite or link to this item:
https://research.matf.bg.ac.rs/handle/123456789/498
Title: | Computer theorem proving for verifiable solving of geometric construction problems | Authors: | Marinković, Vesna Janičić, Predrag Schreck, Pascal |
Affiliations: | Informatics and Computer Science | Issue Date: | 1-Jan-2015 | Related Publication(s): | International Workshop on Automated Deduction in Geometry ADG 2014 | Journal: | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) | Abstract: | Over the last sixty years, a number of methods for automated theorem proving in geometry, especially Euclidean geometry, have been developed. Almost all of them focus on universally quantified theorems. On the other hand, there are only few studies about logical approaches to geometric constructions. Consequently, automated proving of ∀∃ theorems, that correspond to geometric construction problems, have seldom been studied. In this paper, we present a formal logical framework describing the traditional four phases process of geometric construction solving. It leads to automated production of constructions with corresponding human readable correctness proofs. To our knowledge, this is the first study in that direction. In this paper we also discuss algebraic approaches for solving ruler-and-compass construction problems. There are famous problems showing that it is often difficult to prove non-existence of constructible solutions for some tasks. We show how to put into practice well-known algebra-based methods and, in particular, field theory, to prove RC-constructibility in the case of problems from Wernick’s list. |
URI: | https://research.matf.bg.ac.rs/handle/123456789/498 | ISBN: | 9783319213613 | ISSN: | 03029743 | DOI: | 10.1007/978-3-319-21362-0_5 |
Appears in Collections: | Research outputs |
Show full item record
SCOPUSTM
Citations
6
checked on Dec 20, 2024
Page view(s)
21
checked on Dec 24, 2024
Google ScholarTM
Check
Altmetric
Altmetric
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.