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, Morleya 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ą.

Program zajęć

  1. Pakiet komputerowy do obliczeń algebraicznych- wprowadzenie (CoCoA, Maple lub Mathematica)
  2. Wielomiany wielu zmiennych, problem dzielenia z resztą, twierdzenie Hilberta o zerach,
  3. Podstawowe własności baz Groebnera- dlaczego są fajniejsze od innych układów wielomianów
  4. Bezbolesne sprawdzanie czy paskudny układ wielu zmiennych ma rozwiązanie
  5. Sprowadzenie problemu geometrycznego do badania układu równań
  6. Uwzględnianie wyjątków w założeniach, tj przypadki zdegenerowane.
  7. 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.

Wymagania

  • 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
  • Dobre obeznanie z pakietami do obliczeń i umiejętność programowania nie zaszkodzi, ale nie jest konieczna- będziemy używać tylko wybranych poleceń.

Zadania kwalifikacyjne

Dośc obszerny plik z zadaniami jest dostępny tu zadania
Nie ma co się go bać bo oczywiście nie trzeba wszystkiego robić- jest dla tych którzy chcą więcej poćwiczyć, wzbogacony o dużo podpowiedzi :-)
Wstępnie planuję żeby były do zrobienia 4 zadania- jedno obowiązkowo z ostatniego rozdziału.

Dodatkowe informacje i materiały

W razie pytan do treści zadań, niejasności lub innych proszę śmiało mejlować.
Dostępny jest skrypt do warsztatów, a w nim podstawy teoretyczne i przykłady obliczeń komputerowych.
UWAGA: Mała prośba. Jeśli jakieś osoby zainteresowane są warsztatami i programowaniem/algorytmami związanymi z tym tematem proszę o mejla, to pomyślę nad przygotowaniem jakichś dodatkowych interesujących informacji.

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