Automatsko dokazivanje teorema — разлика између измена

Садржај обрисан Садржај додат

Инлајн

Верзија на датум 14. март 2024. у 21:21

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.

While the roots of formalised logic go back to Aristotle, the end of the 19th and early 20th centuries saw the development of modern logic and formalised mathematics. Frege's Begriffsschrift (1879) introduced both a complete propositional calculus and what is essentially modern predicate logic.^[1] His Foundations of Arithmetic, published in 1884,^[2] expressed (parts of) mathematics in formal logic. This approach was continued by Russell and Whitehead in their influential Principia Mathematica, first published 1910–1913,^[3] and with a revised second edition in 1927.^[4] Russell and Whitehead thought they could derive all mathematical truth using axioms and inference rules of formal logic, in principle opening up the process to automatisation. In 1920, Thoralf Skolem simplified a previous result by Leopold Löwenheim, leading to the Löwenheim–Skolem theorem and, in 1930, to the notion of a Herbrand universe and a Herbrand interpretation that allowed (un)satisfiability of first-order formulas (and hence the validity of a theorem) to be reduced to (potentially infinitely many) propositional satisfiability problems.^[5]

In 1929, Mojżesz Presburger showed that the first-order theory of the natural numbers with addition and equality (now called Presburger arithmetic in his honor) is decidable and gave an algorithm that could determine if a given sentence in the language was true or false.^[6]^[7]

However, shortly after this positive result, Kurt Gödel published On Formally Undecidable Propositions of Principia Mathematica and Related Systems (1931), showing that in any sufficiently strong axiomatic system there are true statements that cannot be proved in the system. This topic was further developed in the 1930s by Alonzo Church and Alan Turing, who on the one hand gave two independent but equivalent definitions of computability, and on the other gave concrete examples of undecidable questions.

^ 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.

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.