Klausa Horn

Klausa Horn adalah disjungsi logika literal, di mana paling banyak salah satu literal positif, dan yang lainnya negatif. Ini dinamai Alfred Horn yang menggambarkannya dalam sebuah artikel pada tahun 1951.

Klausa Horn dengan tepat satu literal positif adalah klausa definit; klausa definit tanpa literal negatif kadang-kadang disebut "fakta"; dan klausa Horn tanpa literal positif kadang-kadang disebut klausa tujuan. Ketiga jenis klausa Horn ini diilustrasikan dalam contoh proposisional berikut:

klausa pasti: ¬ p ∨ ¬ q ∨ ⋯ ∨ ¬ t ∨ u {\displaystyle \neg p\lor \neg q\vee \cdots \vee \neg t\vee u} $\neg p\lor \neg q\vee \cdots \vee \neg t\vee u$

fakta: u {\displaystyle u} $u$

klausa tujuan: ¬ p ∨ ¬ q ∨ ⋯ ∨ ¬ t {\displaystyle \neg p\lor \neg q\vee \cdots \vee \neg t} $\neg p\lor \neg q\vee \cdots \vee \neg t$

Dalam kasus non-proposisional, semua variabel dalam klausa secara implisit dikuantifikasi secara universal dengan cakupan seluruh klausa. Jadi, sebagai contoh:

¬ manusia ( X ) ∨ fana ( X ) {\displaystyle \neg {\text{manusia}}(X)\lor {\text{mortal}}(X)} $\neg {\text{human}}(X)\lor {\text{mortal}}(X)$

singkatan dari:

∀ X ( ¬ manusia ( X ) ∨ fana ( X ) ) {\displaystyle \forall X(\neg {\text{human}}(X)\lor {\text{mortal}}(X))} $\forall X(\neg {\text{human}}(X)\lor {\text{mortal}}(X))$

yang secara logika setara dengan:

∀ X ( manusia ( X ) → fana ( X ) ). {\displaystyle \forall X({\text{human}}(X)\rightarrow {\text{mortal}}(X)). } $\forall X({\text{human}}(X)\rightarrow {\text{mortal}}(X)).$

Klausa Horn memainkan peran dasar dalam logika konstruktif dan logika komputasi. Klausa Horn penting dalam pembuktian teorema otomatis dengan resolusi orde pertama, karena resolvent dari dua klausa Horn itu sendiri adalah klausa Horn, dan resolvent dari klausa tujuan dan klausa pasti adalah klausa tujuan. Sifat-sifat klausa Horn ini dapat menyebabkan efisiensi yang lebih besar dalam membuktikan teorema (direpresentasikan sebagai negasi dari klausa tujuan).

Klausa Horn juga merupakan dasar dari pemrograman logika, dimana biasanya klausa definit ditulis dalam bentuk implikasi:

( p ∧ q ∧ ⋯ ∧ t ) → u {\displaystyle (p\wedge q\wedge \cdots \wedge t)\rightarrow u} $(p\wedge q\wedge \cdots \wedge t)\rightarrow u$

Faktanya, resolusi klausa tujuan dengan klausa pasti untuk menghasilkan klausa tujuan baru adalah dasar dari aturan inferensi resolusi SLD, yang digunakan untuk mengimplementasikan pemrograman logika dan bahasa pemrograman Prolog.

Dalam pemrograman logika, klausa pasti berperilaku sebagai prosedur reduksi-tujuan. Sebagai contoh, klausa Horn yang ditulis di atas berperilaku sebagai prosedur:

untuk menunjukkan u {\displaystyle u} $u$ , menunjukkan p {\displaystyle p} $p$ dan menunjukkan q {\displaystyle q} dan ⋯ {\displaystyle \cdots } $\cdots$ dan tunjukkan t {\displaystyle t} $t$ .

Untuk menekankan penggunaan klausa ke belakang ini, sering ditulis dalam bentuk ke belakang:

u ← ( p ∧ q ∧ ⋯ ∧ t ) {\displaystyle u\leftarrow (p\land q\land \cdots \land t)} $u\leftarrow (p\land q\land \cdots \land t)$

Dalam Prolog ini ditulis sebagai:

u :- p, q, ..., t.

Notasi Prolog sebenarnya ambigu, dan istilah "klausa tujuan" kadang-kadang juga digunakan secara ambigu. Variabel-variabel dalam klausa tujuan dapat dibaca sebagai dikuantifikasi secara universal atau eksistensial, dan menurunkan "salah" dapat diartikan baik sebagai menurunkan kontradiksi atau sebagai menurunkan solusi yang berhasil dari masalah yang harus dipecahkan.

Van Emden dan Kowalski (1976) menyelidiki sifat-sifat teoritis model klausa Horn dalam konteks pemrograman logika, menunjukkan bahwa setiap himpunan klausa pasti D memiliki model minimal M. Sebuah rumus atomik A secara logis tersirat oleh D jika dan hanya jika A benar di M. Ini mengikuti bahwa masalah P yang diwakili oleh konjungsi eksistensial terkuantifikasi dari literal positif secara logis tersirat oleh D jika dan hanya jika P benar di M. Model semantik minimal klausa Horn adalah dasar untuk semantik model stabil dari program logika.

Klausa Horn proposisional juga menarik dalam kompleksitas komputasi, dimana masalah menemukan nilai kebenaran untuk membuat konjungsi klausa Horn proposisional menjadi benar adalah masalah P-lengkap (pada kenyataannya dapat dipecahkan dalam waktu linier), kadang-kadang disebut HORNSAT. (Masalah kepuasan Boolean yang tidak terbatas adalah masalah NP-complete). Satisfiability dari klausa Horn orde pertama tidak dapat dipecahkan.

Pertanyaan dan Jawaban

T: Apa yang dimaksud dengan klausa tanduk?

A: Klausa Horn adalah disjungsi logika dari literal, di mana paling banyak salah satu dari literal adalah positif dan yang lainnya negatif.

T: Siapa yang pertama kali mendeskripsikannya?

J: Alfred Horn pertama kali mendeskripsikannya dalam sebuah artikel pada tahun 1951.

T: Apa yang dimaksud dengan klausa pasti?

J: Klausa Horn dengan tepat satu literal positif disebut klausa pasti.

T: Apa yang dimaksud dengan fakta?

J: Klausa pasti tanpa literal negatif terkadang disebut sebagai "fakta".

T: Apa yang dimaksud dengan klausa tujuan?

A: Klausa Horn tanpa literal positif terkadang disebut klausa tujuan.

T: Bagaimana cara kerja variabel dalam kasus non-proposisional?

A: Dalam kasus non-proposisional, semua variabel dalam klausa secara implisit dikuantifikasi secara universal dengan cakupan seluruh klausa. Artinya, variabel-variabel tersebut berlaku untuk setiap bagian dari pernyataan.

T: Peran apa yang dimainkan oleh klausa Horn dalam logika konstruktif dan logika komputasi? J: Klausa Horn memainkan peran penting dalam pembuktian teorema otomatis dengan resolusi orde pertama karena penyelesaian dua klausa Horn atau antara satu tujuan dan satu klausa pasti dapat digunakan untuk menciptakan efisiensi yang lebih besar ketika membuktikan sesuatu yang direpresentasikan sebagai negasi dari klausa tujuannya. Mereka juga digunakan sebagai dasar untuk bahasa pemrograman logika seperti Prolog, di mana mereka berperilaku seperti prosedur reduksi tujuan.