Zautomatyzowanie dowodzenia twierdzeń matematycznych poprzez przeniesienie pracy związanej z procesem decyzyjnym na komputer, wykształciło swoją własną metodologię na styku informatyki, filozofii i matematyki. Najbardziej znanym tego typu przypadkiem jest dowód twierdzenia o czterech barwach, podczas którego do procesu dowodzenia wykorzystano komputer.
Jak obszerny może być taki dowód? Jakie musi spełniać warunki formalne, aby został przyjęty w renomowanym czasopiśmie jako dowód matematyczny? Czy powinien być zrozumiały dla naukowca niebędącego specjalistą w danej dziedzinie? A może ograniczeniem powinna być moc obliczeniowa komputera, na którym został uzyskany? Zapewne odpowiedzi na powyższe pytania straciłyby na znaczeniu, jeżeli otrzymany dowód komputerowy byłby jedynym znanym lub odznaczał się większą elementarnością od klasycznego uzasadnienia bądź naprowadzałby na oryginalną uniwersalną metodę. Czym jest zatem automatyczne dowodzenie twierdzeń (ADT), jak nie rygorystycznym stosowaniem reguł wnioskowania, z tą tylko różnicą, że wykonywanym przez komputer? W obrębie rozległych, złożonych teorii stosowanie ADT może służyć do korekty rozbudowanych rozumowań, otrzymywania alternatywnych dowodów. Niestety na niekorzyść tego podejścia przemawia fakt, że większość tak otrzymywanych rozumowań jest stosunkowo dłuższa od tych wykonywanych klasycznie.
Celem referatu jest przedstawienie automatycznych dowodów wybranych twierdzeń z księgi VI ”Elementów” Euklidesa oraz arytmetyki odcinków opisanej w ”Geometrii” Kartezjusza. Ponadto zostaną zaprezentowane możliwości i ograniczenia zastosowania jednej z metod ADT w geometrii elementarnej, jaką jest metoda pola, za pomocą której otrzymano powyższe przykłady. Do uzyskania automatycznych dowodów twierdzeń wykorzystano środowisko WinGCLC, jedną z implementacji przytoczonej metody.