Geometric Automated Theorem Proving

There are two major families of methods in automated reasoning in geometry: algebraic style and synthetic style methods.

The synthetic methods attempt to automate the traditional proving methods. Many of these methods add auxiliary elements to the geometric configuration considered, so that a certain postulates could apply. This usually leads to a combinatorial explosion of the search space. The challenge is to control the combinatorial explosion and to develop suitable heuristics in order to avoid unnecessary construction steps. Early ruled-based provers were based in artificial intelligence approach, with various degrees of success, but none achieved a reasonable performance. New approaches are currently being proposed.

Algebraic style has its roots in the work of Descartes and in the translation of geometric problems to algebraic problems. The automation of the proving process along this line began with the quantifier elimination method of Tarski and since then had many improvements. All the algebraic methods have in common an algebraic style, unrelated to traditional, synthetic geometry methods, and they do not provide human-readable proofs. Namely, they deal with polynomials that are often extremely complex for a human to understand, and also with no direct link to the geometrical contents.

Other approaches having being implemented, probabilistic provers, coordinate-free methods, coherent logic provers, deductive databases, deductive graphs, etc., with different degrees of success.

Enlarging the scope to the automated deduction and knowledge management in geometry there also many research avenues being pursued.

The implementation of new computational tools, generic or specific to geometry foster many theoretical and applied efforts. The proof assistants, like Coq and Isabelle, enabled effort of formalization in geometry leading to important developments in this area. The dynamic geometry systems lead to many developments: the Formula Derivation, e.g. the automatic determination of the equation of a locus and also the attempt to use deductive databases to find new theorems; the specification of common formats to geometric information interchange and classification; improved geometric provers; geometric search mechanisms; natural language and visual renderings of proofs.

The area of geometric automated theorem proving is a research area very much alive, with many active lines of research. In these four talks the presentation of past, current and foreseeable achievements is presented in the hope of raising the interest, and provoking a lively discussion, to the area of Geometric Automated Theorem Proving.

Talk 1: Geometric Automated Theorem Proving: Introduction and Synthetic Methods.

Talk 2: Geometric Automated Theorem Proving: Algebraic Methods & Semi-synthetic Methods.

Talk 3: Formalization and Mechanical Geometric Formula Derivation.

Talk 4: Geometric Knowledge Management and Computational Tools.

Relatore

Pedro Quaresma (CISUC/Matemathics Department, University of Coimbra, Portugal)

Docente di riferimento

Alessandro Aldini

Vincoli di partecipazione

Non è obbligatoria la partecipazione a tutti i seminari per ottenere i CFU, ma è comunque consigliabile seguire ciascuno solo se si è preso parte ai precedenti.

Date

Luogo Data Orario Crediti (CFU)
Palazzo Albani, Aula D2 16 Gennaio 2019 16:00-18:00 0,125
Palazzo Albani, Aula D2 17 Gennaio 2019 10:00-12:00 0,125
Palazzo Albani, Aula D2 29 Gennaio 2019 16:00-18:00 0,125
Palazzo Albani, Aula D2 30 Gennaio 2019 16:00-18:00 0,125