Automatsko dokazivanje teorema

Automatsko dokazivanje teorema (takođe poznato kao automatizovana dedukcija) je podoblast automatskog zaključivanja i matematičke logike koja se bavi dokazivanjem matematičkih teorema pomoću kompjuterskih programa. Automatsko rezonovanje o matematičkom dokazu bilo je glavni podsticaj za razvoj računarske nauke.

Агда 2 је прооф асистент развијен на технолошком институту Chalmers University of Technology. Ово је снимак текућег доказа у вези са теоријом категорија. Снима се на ЛЦД екрану лаптопа.

Logičke osnove

Dok koreni formalizovane logike sežu do Aristotela, krajem 19. i početkom 20. veka došlo je do razvoja moderne logike i formalizovane matematike. Fregeov Begriffsschrift (1879) uveo je i potpuni propozicioni račun i ono što je u suštini moderna predikatska logika.^[1] Njegove Osnove aritmetike, objavljene 1884. godine,^[2] su izrazile (delove) matematike u formalnoj logici. Ovaj pristup su nastavili Rasel i Vajhed u svojoj uticajnoj Principia Mathematica, koja je prvi put objavljena 1910–1913,^[3] i sa revidiranim drugim izdanjem 1927.^[4] Rasel i Vajthed su smatrali da mogu da formalizuju svu matematičku istinu koristeći aksiome i pravila zaključivanja formalne logike, u principu otvarajući proces automatizaciji. Godine 1920, Toralf Skolem je pojednostavio prethodni rezultat Leopolda Lovenhajma, što je dovelo do Lovenhajm–Skolemove teoreme, a 1930. do pojma Herbrandovog univerzuma i Herbrandove interpretacije koja je dozvoljavala (ne)zadovoljivost formula prvog reda (i stoga valjanost teoreme) da se svede na (potencijalno beskonačno mnogo) problema propozicione zadovoljivosti.^[5]

Godine 1929, Mojžeš Presburger je pokazao da je teorija prvog reda prirodnih brojeva sa sabiranjem i jednakošću (sada u njegovu čast nazvana Presburgerova aritmetika) odlučiva i dao je algoritam koji može da utvrdi da li je data rečenica u jeziku tačna ili netačna.^[6][7]

Međutim, ubrzo nakon ovog pozitivnog rezultata, Kurt Gedel je objavio delo O formalno neodlučivim propozicijama Principia Mathematica i srodnim sistemima (1931), pokazujući da u svakom dovoljno snažnom aksiomatskom sistemu postoje istinite tvrdnje koje se u sistemu ne mogu dokazati. Ovu temu su tridesetih godina prošlog veka dalje razvili Alonzo Čerč i Alan Tjuring, koji su s jedne strane dali dve nezavisne, ali ekvivalentne definicije izračunljivosti, a sa druge konkretne primere neodlučivih pitanja.