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.
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.
Reference[уреди | уреди извор]
- ^ Frege, Gottlob (1879). Begriffsschrift. Verlag Louis Neuert.
- ^ Frege, Gottlob (1884). Die Grundlagen der Arithmetik (PDF). Breslau: Wilhelm Kobner. Архивирано из оригинала (PDF) 2007-09-26. г. Приступљено 2012-09-02.
- ^ Russell, Bertrand; Whitehead, Alfred North (1910—1913). Principia Mathematica (1st изд.). Cambridge University Press.
- ^ Russell, Bertrand; Whitehead, Alfred North (1927). Principia Mathematica (на језику: енглески) (2nd изд.). Cambridge University Press.
- ^ Herbrand, J. (1930). Recherches sur la théorie de la démonstration (PhD) (на језику: француски). University of Paris.
- ^ Presburger, Mojżesz (1929). „Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt”. Comptes Rendus du I Congrès de Mathématiciens des Pays Slaves. Warszawa: 92—101.
- ^ Davis, Martin (2001). „The Early History of Automated Deduction”. Robinson & Voronkov 2001. Архивирано из оригинала 2012-07-28. г. Приступљено 2012-09-08.
Literatura[уреди | уреди извор]
- Chang, Chin-Liang; Lee, Richard Char-Tung (2014) [1973]. Symbolic Logic and Mechanical Theorem Proving. Elsevier. ISBN 9780080917283.
- Loveland, Donald W. (2016) [1978]. Automated Theorem Proving: A Logical Basis. Fundamental Studies in Computer Science. 6. Elsevier. ISBN 9781483296777.
- Luckham, David (1990). Programming with Specifications: An Introduction to Anna, A Language for Specifying Ada Programs. Springer. ISBN 978-1461396871.
- Gallier, Jean H. (2015) [1986]. Logic for Computer Science: Foundations of Automatic Theorem Proving (2nd изд.). Dover. ISBN 978-0-486-78082-5. „This material may be reproduced for any educational purpose, ...”
- Duffy, David A. (1991). Principles of Automated Theorem Proving. Wiley. ISBN 9780471927846.
- Wos, Larry; Overbeek, Ross; Lusk, Ewing; Boyle, Jim (1992). Automated Reasoning: Introduction and Applications (2nd изд.). McGraw–Hill. ISBN 9780079112514.
- Robinson, Alan; Voronkov, Andrei, ур. (2001). Handbook of Automated Reasoning. I. Elsevier, MIT Press. ISBN 9780080532790. II ISBN 9780262182232.
- Fitting, Melvin (2012) [1996]. First-Order Logic and Automated Theorem Proving (2nd изд.). Springer. ISBN 9781461223603.
Spoljašnje veze[уреди | уреди извор]
| Normativna kontrola: Državne |
|---|
