Automated theorem proving (also known as ATP or automated deduction) is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs.
Pembuktian teorema otomatis (juga dikenal sebagai ATP atau deduksi otomatis) adalah cabang dari penalaran otomatis dan logika matematika yang berhubungan dengan pembuktian teorema matematika menggunakan program komputer.
Automated reasoning over mathematical proof was a major motivating factor for the development of computer science.
Penalaran otomatis terhadap bukti matematika merupakan salah satu faktor utama yang mendorong perkembangan ilmu komputer.
While the roots of formalized logic go back to Aristotle, the end of the 19th and early 20th centuries saw the development of modern logic and formalized mathematics.
Meskipun akar logika formal dapat ditelusuri kembali ke Aristoteles, akhir abad ke-19 dan awal abad ke-20 menyaksikan perkembangan logika modern dan matematika formal.
Frege's Begriffsschrift (1879) introduced both a complete propositional calculus and what is essentially modern predicate logic.
Begriffsschrift karya Frege (1879) memperkenalkan baik kalkulus proposisional yang lengkap maupun logika predikat modern pada dasarnya.
His Foundations of Arithmetic, published in 1884, expressed (parts of) mathematics in formal logic.
Foundations of Arithmetic yang diterbitkan pada 1884 mengekspresikan (sebagian) matematika dalam logika formal.
This approach was continued by Russell and Whitehead in their influential Principia Mathematica, first published 1910–1913, and with a revised second edition in 1927.
Pendekatan ini dilanjutkan oleh Russell dan Whitehead dalam karya berpengaruh mereka Principia Mathematica, yang pertama kali diterbitkan antara 1910–1913, dan dengan edisi kedua yang direvisi pada 1927.
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 automation.
Russell dan Whitehead percaya bahwa mereka bisa menurunkan semua kebenaran matematika menggunakan aksioma dan aturan inferensi logika formal, yang pada prinsipnya membuka kemungkinan untuk proses otomatisasi.
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.
Pada 1920, Thoralf Skolem menyederhanakan hasil sebelumnya oleh Leopold Löwenheim, yang menghasilkan teorema Löwenheim–Skolem dan, pada 1930, konsep alam semesta Herbrand (Herbrand universe) dan interpretasi Herbrand (Herbrand interpretation) yang memungkinkan ketidakpuasan atau kepuasan formula orde pertama (dan dengan demikian validitas sebuah teorema) direduksi menjadi masalah kepuasan proposisional yang (potensial) tak terbatas.
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.
Pada 1929, Mojżesz Presburger menunjukkan bahwa teori orde pertama dari bilangan alami dengan operasi penjumlahan dan kesetaraan (yang sekarang disebut aritmetika Presburger untuk menghormatinya) dapat diputuskan dan memberikan algoritma yang dapat menentukan apakah suatu kalimat dalam bahasa tersebut benar atau salah.
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.
Namun, tak lama setelah hasil positif ini, Kurt Gödel menerbitkan On Formally Undecidable Propositions of Principia Mathematica and Related Systems (1931), yang menunjukkan bahwa dalam sistem aksiomatik yang cukup kuat, terdapat pernyataan yang benar tetapi tidak dapat dibuktikan dalam sistem tersebut.
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.
Topik ini kemudian dikembangkan lebih lanjut pada tahun 1930-an oleh Alonzo Church dan Alan Turing, yang di satu sisi memberikan dua definisi komputabilitas yang independen tetapi ekuivalen, dan di sisi lain memberikan contoh konkret dari pertanyaan yang tak dapat diputuskan.
In 1954, Martin Davis programmed Presburger's algorithm for a JOHNNIAC vacuum-tube computer at the Institute for Advanced Study in Princeton, New Jersey.
Pada tahun 1954, Martin Davis memprogram algoritma Presburger untuk komputer tabung vakum JOHNNIAC di Institute for Advanced Study di Princeton, New Jersey.
More ambitious was the Logic Theorist in 1956, a deduction system for the propositional logic of the Principia Mathematica, developed by Allen Newell, Herbert A. Simon and J. C. Shaw.
Lebih ambisius lagi adalah Logic Theorist pada tahun 1956, sebuah sistem deduksi untuk logika proposisional dari Principia Mathematica, yang dikembangkan oleh Allen Newell, Herbert A. Simon, dan J. C. Shaw.
Also running on a JOHNNIAC, the Logic Theorist constructed proofs from a small set of propositional axioms and three deduction rules: modus ponens, (propositional) variable substitution, and the replacement of formulas by their definition.
Juga dijalankan pada JOHNNIAC, Logic Theorist menyusun bukti dari sekumpulan kecil aksioma proposisional dan tiga aturan deduksi: modus ponens, substitusi variabel (proposisional), dan penggantian formula dengan definisinya.
The system used heuristic guidance, and managed to prove 38 of the first 52 theorems of the Principia.
Sistem ini menggunakan panduan heuristik, dan berhasil membuktikan 38 dari 52 teorema pertama dari Principia Mathematica.
The "heuristic" approach of the Logic Theorist tried to emulate human mathematicians, and could not guarantee that a proof could be found for every valid theorem even in principle.
Pendekatan “heuristik” Logic Theorist mencoba meniru cara matematikawan manusia, dan tidak dapat menjamin bahwa bukti dapat ditemukan untuk setiap teorema yang valid, bahkan secara prinsip.
In contrast, other, more systematic algorithms achieved, at least theoretically, completeness for first-order logic.
Sebaliknya, algoritma lain yang lebih sistematis mampu mencapai, setidaknya secara teoretis, kelengkapan untuk logika orde pertama.
Initial approaches relied on the results of Herbrand and Skolem to convert a first-order formula into successively larger sets of propositional formulae by instantiating variables with terms from the Herbrand universe.
Pendekatan awal bergantung pada hasil Herbrand dan Skolem untuk mengubah sebuah formula orde pertama menjadi himpunan formula proposisional yang semakin besar dengan mengganti variabel menggunakan istilah dari alam semesta Herbrand.
Gilmore's program used conversion to disjunctive normal form, a form in which the satisfiability of a formula is obvious.
Program Gilmore menggunakan konversi ke bentuk normal disjungtif (disjunctive normal form), sebuah bentuk di mana kepuasan suatu formula menjadi jelas.