Mengapa penyatuan sangat penting bagi mesin inferensi?

^{Saya belajar Pembuktian Teorema Otomatis / Pemecah SMT / Asisten Bukti sendiri dan memposting serangkaian pertanyaan tentang prosesnya, mulai dari sini .}

Saya terus membaca tentang Algoritma Unifikasi .

• Apa itu dan mengapa begitu penting untuk Inference Engine ?
• Mengapa begitu penting bagi Ilmu Komputer?

Unifikasi adalah konsep dasar dalam ilmu komputer yang mungkin pada saat itu kita anggap remeh. Setiap kali kita memiliki aturan atau persamaan atau pola dan ingin menerapkannya pada beberapa data, penyatuan digunakan untuk mengkhususkan aturan tersebut pada data. Atau jika kita ingin menggabungkan dua aturan umum namun tumpang tindih, penyatuan memberi kita aturan gabungan paling umum. Unifikasi adalah inti dari

• Pembukti teorema dan asisten bukti, termasuk beberapa berdasarkan penyatuan tingkat tinggi.
• Implementasi prolog (sebagai Resolusi).
• Ketik algoritma inferensi.
• Komputasi linguistik / pemrosesan bahasa alami.
• Istilah sistem penulisan ulang seperti Maude, yang dapat digunakan sebagai dasar semantik bahasa pemrograman.
• Basis data khusus.
• Sistem pakar atau lebih umum Kecerdasan buatan.
• Sistem aljabar komputer.
• Pencocokan pola dalam bahasa fungsional (setidaknya sebagian ... hanya pencocokan).
• Beberapa pendekatan parsing.
• Beberapa bahasa permintaan, terutama yang melibatkan Web Semantik.

Asisten pembuktian seperti Isabelle / HOL bekerja pada level sintaksis pada kalkulus logis. Bayangkan Anda memiliki aturan mode ponens (MP)

$\qquad \displaystyle P\to Q, P\ \Longrightarrow\ Q$

dan tujuan buktinya

$\qquad \displaystyle (a \lor b) \to (c \land d), a \lor b \ \overset{!}{\Longrightarrow} c\land d$

Kita manusia segera melihat bahwa ini mengikuti dengan modus ponens, tetapi mesin harus mencocokkan tujuan untuk memerintah secara sintaksis (apakah Anda melakukannya apply rule mpatau apply simp), dan inilah yang dilakukan unifikasi. Algoritma menemukan dengan φ ( P ) = $\varphi$ dan φ ( Q ) = c ∧ d , membuat aturan dan menerapkannya.$\varphi(P) = a\lor b$$\varphi(Q) = c \land d$

Hal yang baik tentang metode asisten seperti simpsekarang adalah jika tujuan Anda adalah

$\qquad \displaystyle (a \lor b) \to (c \land d), a \ \overset{!}{\Longrightarrow} d$

bahwa mereka akan menemukan urutan aplikasi aturan MP yang sesuai, dan P ⟹ P ∨ Q dengan unifikasi yang kompatibel untuk langkah masing-masing dan menyelesaikan tujuan.$P \land Q \Longrightarrow P$$P \Longrightarrow P \lor Q$

Notasi: Dengan satu set rumus logis, notasi$\Gamma = \{\varphi_1, \dots, \varphi_n\}$

$\qquad \Gamma \Longrightarrow \psi$

berarti yang berikut:

Jika saya telah menurunkan / membuktikan semua rumus dalam (yaitu valid ) maka aturan ini menyatakan bahwa ψ juga valid.$\Gamma$$\psi$

Dalam arti tertentu, aturan adalah langkah terakhir dalam bukti (panjang) untuk ψ . Bukti hanyalah rantai aplikasi aturan semacam itu.$\Gamma \Longrightarrow \psi$$\psi$

Perhatikan bahwa aturan biasanya berisi variabel skematik ( dan Q di atas) yang dapat diganti dengan rumus sewenang-wenang asalkan variabel yang sama diganti dengan rumus yang sama di semua contoh; hasil dari format itu adalah contoh aturan konkret (atau secara intuitif, langkah pembuktian). Penggantian ini di atas dilambangkan dengan φ yang ditemukan oleh unifikasi.$P$$Q$$\varphi$

Seringkali orang menggunakan alih-alih ⟹ .$\models$$\Longrightarrow$

Saya tidak berpikir itu penting untuk mesin inferensi . Algoritme unifikasi sangat membantu untuk inferensi tipe . Ini adalah dua jenis kesimpulan yang sangat berbeda.

Jenis inferensi penting untuk ilmu komputer karena jenis penting dalam teori bahasa pemrograman, yang merupakan bagian penting dari ilmu komputer. Tipe juga dekat dengan logika dan digunakan secara intensif dalam pembuktian teorema otomatis. Ada implementasi algoritma unifikasi di banyak, jika tidak semua, asisten bukti dan pemecah SMT.

Mesin inferensi berhubungan dengan kecerdasan buatan, yang juga penting tetapi sangat berbeda. (Saya telah melihat hubungan antara belajar dan logika tetapi ini tampaknya diambil.)