Automatyczne Dowodzenie w Geometrii

Prowadzący: Maciej Skórski.

Opis

Na warsztatach nauczymy się jak za pomocą komputera można dowodzić twierdzeń z elementarnej geometrii (a także próbować ich poszukiwać).

Zagadnienie automatycznego dowodzenia twierdzeń goemetrycznych rozwija się intensywnie od lat 80tych. Stosowane podejścia można ogólnie podzielić na algebraiczne oraz AI (sztuczna inteligencja). Popularne implementacje pierwszego podejścia sprowadzają się do "twardych" obliczeń symbolicznych, drugie próbują generować dowody przez konstrukcje geometryczne- naśladując sposób rozumowania człowieka.

Podczas zajęć zajmiemy się pierwszym podejściem, prezentując jedną z podstawowych technik algebraicznego dowodzenia w geometrii- poprzez badanie układów równań wielu zmiennych, oraz jej praktyczne zastosowania.
Metoda ma pewne ograniczenia o których opowiem, niemniej jednak za jej pomocą można dowieść na przykład twierdzeń Cevy, Pappusa, Steinera, Apoloniusza i wielu innych, a także zaadoptować do poszukiwania (wykrywania) twierdzeń.

Jest to technologia idealna dla osób robiących zadania z geometrii z tzw. buta, to znaczy przez geometrię analityczną.

Ramowy plan zajęć

  • Pakiet komputerowy do obliczeń algebraicznych- wprowadzenie
  • Wielomiany wielu zmiennych, problem dzielenia z resztą, twierdzenie Hilberta o zerach,
  • Podstawowe własności baz Groebnera- dlaczego są fajniejsze od innych układów wielomianów
  • Jak bezboleśnie sprawdzić czy paskudny układ wielu zmiennych ma rozwiązanie?
  • Sprowadzenie problemu geometrycznego do układu równań
  • Uwzględnianie wyjątków w założeniach, tj przypadki zdegenerowane.
  • Rozwalanie zadanek goemetrycznych :-)

Zajęcia mają na celu pokazać jak działa algebraiczny silnik metody oraz jej zastosowanie. Podejście choć proste w idei, opiera się o niebanalne fakty z algebry np twierdzenie Hilberta o zerach, algorytmy obliczania baz Groebnera. Nie będziemy zagłębiać się w ich analizę i dowody- skupimy się przede wszystkim na zastosowaniach w obliczeniach komputerowych. Rozszerzone wiadomości będą dostępne dla zainteresowanych w dodatku do skryptu.

Oczekiwane od uczestników :-)

  • Dobra znajomość wielomianów jednej zmiennej: dzielenie z resztą, obliczanie NWD, zasadnicze twierdzenie algebry.
  • Sprawność (jako taka) w przkształcaniu wyrażeń algebraicznych, układów równań itp
  • Dobra znajomość szkolnej geometrii analitycznej- podział odcinka w proporcji, prostopadłość, równoległość, okrąg, styczna
  • Podzielanie poglądu, że eleganckie rozwiązywanie geometrii jest strasznie trudne

Zapraszam zainteresowanych algebrą i informatyką teoretyczną.
Uwaga: Nie jest konieczna umiejętność programowania.

Meteriały i zadania kwalifikacyjne

Skrypt i zadania kwalifikacyjne dostępne będą, prawdopodobnie około połowy maja.

O ile nie zaznaczono inaczej, treść tej strony objęta jest licencją Creative Commons Attribution-ShareAlike 3.0 License