Opis
Automatyczne dowodzenie twierdzeń
geometrycznych metodą Wu
Szymon Bizoń , Jakub Chmiel
Abstrakt
Metoda Wu to algorytmiczna technika automatycznego dowodze-
nia twierdzeń geometrycznych, oparta na tłumaczeniu założeń geo-
metrycznych na układy równań wielomianowych i analizie tych ukła-
dów z czysto algebraicznego punktu widzenia. W referacie omówimy
pojęcia i fakty kluczowe dla metody Wu (pseudodzielenie, łańcuchy
wstępujące, zbiory charakterystyczne, zasada Ritta) oraz procedurę
sprowadzania układu równań wielomianowych do postaci trójkątnej.
Wyjaśnimy krok po kroku, jak przetłumaczyć przykładowe twierdze-
nie geometryczne na język wielomianów. Następnie pokażemy, w jaki
sposób odpowiedni program automatycznie przeprowadza dowód te-
go twierdzenia (albo stwierdza, że jest ono fałszywe). Zaprezentujemy
też krótką implementację algorytmu sukcesywnego pseudodzielenia w
Pythonie z użyciem biblioteki SymPy. Na koniec porównamy zalety i
ograniczenia metody Wu oraz wskażemy pewne inne obszary jej za-
stosowań
