Dimostrazioni automatiche di teoremi geometrici mediante basi di Groebner

Automatic proofs consist in algorithms that allow a computer to formally proove mathematical theorems. The Groebner basis method allows the computer to automate the proof of Euclidean geometry theorems. It is based on the translation of a statement into polynomials with the aim of study the ideal generated by these polynomials with a powerful algebraic tool, the Groebner bases. The dissertation exposes the algorithm, highlight some limitations and proves a well-known theorem of Euclidean geometry with this algorithm.

Le dimostrazioni automatiche consistono, in generale, in algoritmi che permettono di dimostrare formalmente teoremi matematici tramite un calcolatore. Il metodo delle basi di Groebner permette di automatizzare la dimostrazione di teoremi di geometria euclidea. Esso si basa sulla traduzione di un enunciato in polinomi col fine di poter studiare l'ideale generato da tali polinomi con un potente strumento algebrico, le basi di Groebner appunto. Nella dissertazione si espone l'algoritmo, evidendone alcune limitazioni, e lo si applica per dimostrare un noto teorema di geometria euclidea.