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.

Reference

  1. ^ Frege, Gottlob (1879). Begriffsschrift. Verlag Louis Neuert. 
  2. ^ Frege, Gottlob (1884). Die Grundlagen der Arithmetik (PDF). Breslau: Wilhelm Kobner. Архивирано из оригинала (PDF) 2007-09-26. г. Приступљено 2012-09-02. 
  3. ^ Russell, Bertrand; Whitehead, Alfred North (1910—1913). Principia Mathematica (1st изд.). Cambridge University Press. 
  4. ^ Russell, Bertrand; Whitehead, Alfred North (1927). Principia Mathematica (на језику: енглески) (2nd изд.). Cambridge University Press. 
  5. ^ Herbrand, J. (1930). Recherches sur la théorie de la démonstration (PhD) (на језику: француски). University of Paris. 
  6. ^ 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. 
  7. ^ 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

  • A list of theorem proving tools
Normativna kontrola: Državne Уреди на Википодацима
  • Izrael
  • Sjedinjene Države