Estudo Geralhttps://estudogeral.uc.ptThe DSpace digital repository system captures, stores, indexes, preserves, and distributes digital research material.Tue, 15 Oct 2024 23:19:40 GMT2024-10-15T23:19:40Z5051Towards a Geometry Automated Provers Competitionhttps://hdl.handle.net/10316/105903Title: Towards a Geometry Automated Provers Competition
Authors: Baeta, Nuno; Quaresma, Pedro; Kovács, Zoltán
Abstract: The geometry automated theorem proving area distinguishes itself by a large
number of specific methods and implementations, different approaches
(synthetic, algebraic, semi-synthetic) and different goals and applications
(from research in the area of artificial intelligence to applications in
education).
Apart from the usual measures of efficiency (e.g. CPU time), the possibility
of visual and/or readable proofs is also an expected output against which the
geometry automated theorem provers (GATP) should be measured.
The implementation of a competition between GATP would allow to create a test
bench for GATP developers to improve the existing ones and to propose new ones.
It would also allow to establish a ranking for GATP that could be used by
"clients" (e.g. developers of educational e-learning systems) to choose the
best implementation for a given intended use.
Description: In Proceedings ThEdu'19, arXiv:2002.11895
Fri, 28 Feb 2020 00:00:00 GMThttps://hdl.handle.net/10316/1059032020-02-28T00:00:00ZO método do ângulo completo no sistema OpenGeoProverhttps://hdl.handle.net/10316/47639Title: O método do ângulo completo no sistema OpenGeoProver
Authors: Baeta, Nuno Miguel dos Santos
Abstract: O método do ângulo completo para geometria euclideana construtiva foi proposto por Chou, Gao e Zhang no início dos anos 1990. Este método, uma extensão do método da área proposto pelos mesmos autores, produz demonstrações legíveis e de um modo eficiente demonstra muitos teoremas não triviais. Pode ser considerado como um dos métodos mais interessante e de maior sucesso na demonstração de teoremas em geometria e, possivelmente, o mais bem sucedido na produção de demonstrações automáticas legíveis. Nesta dissertação de mestrado faz-se a apresentação do mêtodo do ângulo completo e demonstram-se muitos dos seus lemas. Descreve-se ainda a planificação da implementação, em código livre, do método do ângulo completo.; The full-angle method for euclidean constructive geometry was proposed by Chou, Gao, Zhang in early 1990’s. The method, an extension of the area method proposed by the same authors, produces humanreadable proofs and can efficiently prove many non-trivial theorems. It can be considered as one of the most interesting and most successful methods in geometry theorem proving and probably the most successful in the domain of automated production of readable proofs. In this master thesis a presentation of the full-angle method is made and several of its lemmas are proved. A plannification of the implementation, in open source code, of the full-angle method is also described.
Description: Dissertação de Mestrado em Matemática apresentada à Faculdade de Ciências e Tecnologia da Universidade de Coimbra
Mon, 17 Jun 2013 00:00:00 GMThttps://hdl.handle.net/10316/476392013-06-17T00:00:00ZTowards Ranking Geometric Automated Theorem Provershttps://hdl.handle.net/10316/106878Title: Towards Ranking Geometric Automated Theorem Provers
Authors: Baeta, Nuno; Quaresma, Pedro
Abstract: The field of geometric automated theorem provers has a long and rich history,
from the early AI approaches of the 1960s, synthetic provers, to today
algebraic and synthetic provers.
The geometry automated deduction area differs from other areas by the strong
connection between the axiomatic theories and its standard models. In many
cases the geometric constructions are used to establish the theorems'
statements, geometric constructions are, in some provers, used to conduct the
proof, used as counter-examples to close some branches of the automatic proof.
Synthetic geometry proofs are done using geometric properties, proofs that can
have a visual counterpart in the supporting geometric construction.
With the growing use of geometry automatic deduction tools as applications in
other areas, e.g. in education, the need to evaluate them, using different
criteria, is felt. Establishing a ranking among geometric automated theorem
provers will be useful for the improvement of the current
methods/implementations. Improvements could concern wider scope, better
efficiency, proof readability and proof reliability.
To achieve the goal of being able to compare geometric automated theorem
provers a common test bench is needed: a common language to describe the
geometric problems; a comprehensive repository of geometric problems and a set
of quality measures.
Description: In Proceedings ThEdu'18, arXiv:1903.12402
Mon, 01 Apr 2019 00:00:00 GMThttps://hdl.handle.net/10316/1068782019-04-01T00:00:00ZExchange of Geometric Information Between Applicationshttps://hdl.handle.net/10316/107546Title: Exchange of Geometric Information Between Applications
Authors: Quaresma, Pedro; Santos, Vanda; Baeta, Nuno
Abstract: The Web Geometry Laboratory (WGL) is a collaborative and adaptive e-learning
Web platform integrating a well known dynamic geometry system. Thousands of
Geometric problems for Geometric Theorem Provers (TGTP) is a Web-based
repository of geometric problems to support the testing and evaluation of
geometric automated theorem proving systems.
The users of these systems should be able to profit from each other. The TGTP
corpus must be made available to the WGL user, allowing, in this way, the
exploration of TGTP problems and their proofs. On the other direction TGTP
could gain by the possibility of a wider users base submitting new problems.
Such information exchange between clients (e.g. WGL) and servers (e.g. TGTP)
raises many issues: geometric search - someone, working in a geometric problem,
must be able to ask for more information regarding that construction; levels of
geometric knowledge and interest - the problems in the servers must be
classified in such a way that, in response to a client query, only the problems
in the user's level and/or interest are returned; different aims of each tool -
e.g. WGL is about secondary school geometry, TGTP is about formal proofs in
semi-analytic and algebraic proof methods, not a perfect match indeed;
localisation issues, e.g. a Portuguese user obliged to make the query and
process the answer in English; technical issues-many technical issues need to
be addressed to make this exchange of geometric information possible and
useful.
Instead of a giant (difficult to maintain) tool, trying to cover all, the
interconnection of specialised tools seems much more promising. The challenges
to make that connection work are many and difficult, but, it is the authors
impression, not insurmountable.
Description: In Proceedings ThEdu'17, arXiv:1803.00722
Mon, 05 Mar 2018 00:00:00 GMThttps://hdl.handle.net/10316/1075462018-03-05T00:00:00ZOpen Geometry Prover Community Projecthttps://hdl.handle.net/10316/103873Title: Open Geometry Prover Community Project
Authors: Baeta, Nuno; Quaresma, Pedro
Abstract: Mathematical proof is undoubtedly the cornerstone of mathematics. The
emergence, in the last years, of computing and reasoning tools, in particular
automated geometry theorem provers, has enriched our experience with
mathematics immensely. To avoid disparate efforts,the Open Geometry Prover
Community Project aims at the integration of the different efforts for the
development of geometry automated theorem provers, under a common "umbrella".
In this article the necessary steps to such integration are specified and the
current implementation of some of those steps is described.
Description: In Proceedings ADG 2021, arXiv:2112.14770
Mon, 03 Jan 2022 00:00:00 GMThttps://hdl.handle.net/10316/1038732022-01-03T00:00:00Z