Apa kekurangan dari prosedur resolusi Robinson?

Aug 16 2020

Paulson dkk. Dari LCF ke Isabelle / HOL katakan:

Resolusi untuk logika urutan pertama, lengkap pada prinsipnya tetapi dalam praktiknya sering kali mengecewakan.

Saya pikir lengkap berarti mereka dapat membuktikan formula yang benar dalam logika orde pertama yang benar. Dalam Handbook of Automated Reasoning saya menemukan:

Resolusi adalah metode pembuktian teorema lengkap yang dapat disangkal: sebuah kontradiksi (yaitu, klausa kosong) dapat disimpulkan dari sekumpulan klausa yang tidak memuaskan.

Dari Wikipedia:

Mencoba membuktikan formula orde pertama yang memuaskan sebagai tidak memuaskan dapat mengakibatkan penghitungan yang tidak dapat dihentikan

Mengapa itu mengecewakan?

Jawaban

1 cody Aug 20 2020 at 00:26

Meskipun "mengecewakan dalam praktiknya" tentu tidak dapat didefinisikan secara formal, tidak seperti "lengkap" (yang memang berarti "pada akhirnya dapat membuktikan setiap formula yang benar"), cukup mudah untuk menemukan contoh di mana resolusi naif bahkan tidak memadai dari jarak jauh, yaitu contoh yang seharusnya mudah dibuktikan tetapi resolusi mana yang sangat lambat.

Contoh terkenal adalah pengkodean prinsip lubang merpati untuk$n$ lubang dalam logika proposisional (yang merupakan pernyataan "$n+1$ merpati tidak bisa masuk $n$lubang tanpa duplikat). Tidak ada bukti pernyataan ini hanya menggunakan resolusi dalam waktu sub-eksponensial dalam$n$.

Hal-hal bahkan lebih buruk dalam logika predikat, di mana sangat mudah untuk menemukan pernyataan tanpa bukti resolusi yang cepat.

Perhatikan bahwa setiap implementasi resolusi harus menerapkan strategi untuk memilih resolven, yang sudah menjadi masalah yang sangat sulit, dan area penelitian aktif, karena kebanyakan algoritma praktis untuk pembuktian teorema adalah peningkatan resolusi naif, misalnya resolusi hiper .