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} 
fakta: u {\displaystyle u} 
klausa tujuan: ¬ p ∨ ¬ q ∨ ⋯ ∨ ¬ t {\displaystyle \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)} 
singkatan dari:
∀ X ( ¬ manusia ( X ) ∨ fana ( X ) ) {\displaystyle \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)). } 
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} 
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} , menunjukkan p {\displaystyle p}
dan menunjukkan q {\displaystyle q}
dan ⋯ {\displaystyle \cdots } 
dan tunjukkan t {\displaystyle 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)} 
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.