Apakah ada perangkat lunak untuk secara otomatis memvalidasi argumen?

Dec 20 2020

aku suka untuk

  1. Dapatkan argumen logis dari bahasa Inggris, dan
  2. uji validitasnya menggunakan program.

Apakah ada perangkat lunak untuk langkah 2? Akan baik-baik saja jika menyerah karena

  1. Validitas tidak dapat dihitung, atau
  2. butuh waktu lama untuk melaporkan hasilnya.

Saya menyadari bahwa menanyakan pertanyaan ini dapat mengungkapkan ketidaktahuan saya tentang logika, jadi jika itu pertanyaan konyol, saya akan berterima kasih atas beberapa referensi yang menjelaskan mengapa demikian. Saya akan mulai dengan Metalogic: An Introduction to the Metatheory of Standard First Order .

Jawaban

13 lemontree Dec 20 2020 at 22:34

Anda sedang mencari apa yang disebut prover teorema otomatis .

Lihat misalnya pyPL atau Tree Proof Generator untuk dua implementasi kalkulus tabel analitik untuk logika proposisional klasik dan orde pertama.

Kalkulus tablo selesai untuk validitas orde pertama, yang berarti bahwa setiap inferensi yang valid akan dideteksi seperti itu.
Tetapi logika orde pertama bukanlah co-semi-decidable, yang berarti bahwa tidak mungkin menemukan algoritme yang akan mendeteksi semua non-inferensi seperti itu; pada beberapa kesimpulan yang tidak valid, algoritma tablo akan mengalami tak terhingga.
Sebaliknya, logika proposisional sepenuhnya dapat diputuskan; algoritma tablo pada akhirnya akan mendeteksi semua argumen proposisional yang valid dan semua tidak valid.

Juga ada kendala kompleksitas; Pohon tablo sangat rentan terhadap ledakan kombinatorial kecuali jika heuristik canggih diterapkan, sehingga kedua program di atas hanya akan bekerja secara realistis untuk argumen yang relatif sederhana.

Penerapan banyak sistem pembuktian lainnya telah dilakukan juga. Wikipedia mencantumkan banyak, tetapi saya sendiri belum pernah mengerjakannya sehingga Anda harus memeriksa mana yang cocok untuk kasus penggunaan non-akademik dan non-industri.