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. Njegove Osnove aritmetike, objavljene 1884. godine, 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, i sa revidiranim drugim izdanjem 1927. 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.

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.

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.

Reference

Literatura

.

Spoljašnje veze A list of theorem proving tools

Категорија:Теоријско рачунарство Категорија:Информатика