Please use this identifier to cite or link to this item:
https://research.matf.bg.ac.rs/handle/123456789/510
DC Field | Value | Language |
---|---|---|
dc.contributor.author | Janičić, Predrag | en_US |
dc.contributor.author | Narboux, Julien | en_US |
dc.contributor.author | Quaresma, Pedro | en_US |
dc.date.accessioned | 2022-08-13T10:14:42Z | - |
dc.date.available | 2022-08-13T10:14:42Z | - |
dc.date.issued | 2012-01-01 | - |
dc.identifier.issn | 01687433 | en |
dc.identifier.uri | https://research.matf.bg.ac.rs/handle/123456789/510 | - |
dc.description.abstract | The area method for Euclidean constructive geometry was proposed by Chou, Gao and Zhang in the early 1990's. The method can efficiently prove many non-trivial geometry theorems and is one of the most interesting and most successful methods for automated theorem proving in geometry. The method produces proofs that are often very concise and human-readable. In this paper, we provide a first complete presentation of the method. We provide both algorithmic and implementation details that were omitted in the original presentations. We also give a variant of Chou, Gao and Zhang's axiom system. Based on this axiom system, we proved formally all the lemmas needed by the method and its soundness using the Coq proof assistant. To our knowledge, apart from the original implementation by the authors who first proposed the method, there are only three implementations more. Although the basic idea of the method is simple, implementing it is a very challenging task because of a number of details that has to be dealt with. With the description of the method given in this paper, implementing the method should be still complex, but a straightforward task. In the paper we describe all these implementations and also some of their applications. © Springer Science+Business Media B.V. 2010. | en |
dc.relation.ispartof | Journal of Automated Reasoning | en |
dc.subject | Area method | en |
dc.subject | Automated theorem proving | en |
dc.subject | Formalisation | en |
dc.subject | Geometry | en |
dc.title | The area method: A recapitulation | en_US |
dc.type | Article | en_US |
dc.identifier.doi | 10.1007/s10817-010-9209-7 | - |
dc.identifier.scopus | 2-s2.0-84864955220 | - |
dc.identifier.url | https://api.elsevier.com/content/abstract/scopus_id/84864955220 | - |
dc.contributor.affiliation | Informatics and Computer Science | en_US |
dc.relation.firstpage | 489 | en |
dc.relation.lastpage | 532 | en |
dc.relation.volume | 48 | en |
dc.relation.issue | 4 | en |
item.fulltext | No Fulltext | - |
item.openairecristype | http://purl.org/coar/resource_type/c_18cf | - |
item.cerifentitytype | Publications | - |
item.grantfulltext | none | - |
item.openairetype | Article | - |
crisitem.author.dept | Informatics and Computer Science | - |
crisitem.author.orcid | 0000-0001-8922-4948 | - |
Appears in Collections: | Research outputs |
SCOPUSTM
Citations
45
checked on Dec 20, 2024
Page view(s)
15
checked on Dec 24, 2024
Google ScholarTM
Check
Altmetric
Altmetric
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.