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. Penalaran otomatis terhadap bukti matematika merupakan salah satu faktor utama yang mendorong perkembangan ilmu komputer.

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.^[1] Begriffsschrift karya Frege (1879) memperkenalkan baik kalkulus proposisional yang lengkap maupun logika predikat modern pada dasarnya. Foundations of Arithmetic yang diterbitkan pada 1884 mengekspresikan (sebagian) matematika dalam logika formal.^[2] Pendekatan ini dilanjutkan oleh Russell dan Whitehead dalam karya berpengaruh mereka Principia Mathematica, yang pertama kali diterbitkan antara 1910–1913,^[3] dan dengan edisi kedua yang direvisi pada 1927.^[4] 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.

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.

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.^[5][6]

Namun, tak lama setelah hasil positif ini, Kurt Gödel menerbitkan On Formally Undecidable Propositions of Principia Mathematica and Related Systems (1931),^[7] yang menunjukkan bahwa dalam sistem aksiomatik yang cukup kuat, terdapat pernyataan yang benar tetapi tidak dapat dibuktikan dalam sistem tersebut. 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.^[8]

Pada tahun 1954, Martin Davis memprogram algoritma Presburger untuk komputer tabung vakum JOHNNIAC di Institute for Advanced Study di Princeton, New Jersey. Menurut Davis, “Keberhasilan besarnya adalah membuktikan bahwa jumlah dua bilangan genap adalah genap.”^[6]

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. 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. Sistem ini menggunakan panduan heuristik, dan berhasil membuktikan 38 dari 52 teorema pertama dari Principia Mathematica.^[5]

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. Sebaliknya, algoritma lain yang lebih sistematis mampu mencapai, setidaknya secara teoretis, kelengkapan untuk logika orde pertama. 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. Formula proposisional tersebut kemudian dapat diperiksa ketidakpuasannya menggunakan berbagai metode. Program Gilmore menggunakan konversi ke bentuk normal disjungtif (disjunctive normal form), sebuah bentuk di mana kepuasan suatu formula menjadi jelas.^[9]