Bir Horn cümlesi, değişmezlerden en fazla birinin pozitif ve diğerlerinin negatif olduğu değişmezlerin mantıksal bir ayrımıdır. Adını 1951 yılında bir makalede tanımlayan Alfred Horn'dan almıştır.
Tam olarak bir pozitif değişmezi olan bir Horn cümlesi kesin bir cümledir; negatif değişmezi olmayan kesin bir cümle bazen "gerçek" olarak adlandırılır; ve pozitif değişmezi olmayan bir Horn cümlesi bazen bir amaç cümlesi olarak adlandırılır. Bu üç çeşit Horn cümlesi aşağıdaki önerme örneğinde gösterilmiştir:
kesin cümle: ¬ p ∨ ¬ q ∨ ⋯ ∨ ¬ t ∨ u {\displaystyle \neg p\lor \neg q\vee \cdots \vee \neg t\vee u} 
fact: u {\displaystyle u} 
hedef maddesi: ¬ p ∨ ¬ q ∨ ⋯ ∨ ¬ t {\displaystyle \neg p\lor \neg q\vee \cdots \vee \neg t} 
Önermesel olmayan durumda, bir tümcede yer alan tüm değişkenler, tümcenin tamamını kapsayacak şekilde örtük olarak evrensel olarak nicelenir. Böylece, örneğin:
¬ human ( X ) ∨ mortal ( X ) {\displaystyle \neg {\text{human}}(X)\lor {\text{mortal}}(X)} 
anlamına gelir:
∀ X ( ¬ insan ( X ) ∨ ölümlü ( X ) ) {\displaystyle \forall X(\neg {\text{human}}(X)\lor {\text{mortal}}(X))} 
mantıksal olarak eşdeğerdir:
∀ X ( insan ( X ) → ölümlü ( X ) ) . {\displaystyle \forall X({\text{human}}(X)\rightarrow {\text{mortal}}(X)). } 
Horn cümleleri, yapısal mantık ve hesaplamalı mantıkta temel bir rol oynar. Birinci dereceden çözümleme ile otomatik teorem kanıtlamada önemlidirler, çünkü iki Horn cümlesinin çözümleyicisinin kendisi bir Horn cümlesidir ve bir amaç cümlesinin ve bir kesin cümlenin çözümleyicisi bir amaç cümlesidir. Horn tümcelerinin bu özellikleri, bir teoremin (bir amaç tümcesinin olumsuzlaması olarak temsil edilir) kanıtlanmasında daha fazla verimlilik sağlayabilir.
Horn cümleleri aynı zamanda mantık programlamanın da temelini oluşturur; burada kesin cümlelerin bir çıkarım şeklinde yazılması yaygındır:
( p ∧ q ∧ ⋯ ∧ t ) → u {\displaystyle (p\wedge q\wedge \cdots \wedge t)\rightarrow u} 
Aslında, yeni bir hedef cümle üretmek için bir hedef cümlenin kesin bir cümle ile çözümlenmesi, mantık programlama ve programlama dili Prolog'u uygulamak için kullanılan SLD çözümleme çıkarım kuralının temelidir.
Mantık programlamada belirli bir cümle, bir hedef azaltma prosedürü gibi davranır. Örneğin, yukarıda yazılan Horn cümlesi prosedür gibi davranır:
u {\displaystyle u} , p {\displaystyle p}
ve q {\displaystyle q}
ve ⋯ {\displaystyle \cdots } göstermek için 
ve show t {\displaystyle t}
.
Cümlenin bu geriye doğru kullanımını vurgulamak için, genellikle geriye doğru biçiminde yazılır:
u ← ( p ∧ q ∧ ⋯ ∧ t ) {\displaystyle u\leftarrow (p\land q\land \cdots \land t)} 
Prolog'da bu şu şekilde yazılır:
u :- p, q, ..., t.Prolog notasyonu aslında belirsizdir ve "hedef cümle" terimi de bazen belirsiz bir şekilde kullanılır. Bir hedef cümlesindeki değişkenler evrensel veya varoluşsal olarak nicelenmiş olarak okunabilir ve "yanlış" türetmek bir çelişki türetmek veya çözülecek problemin başarılı bir çözümünü türetmek olarak yorumlanabilir.
Van Emden ve Kowalski (1976) mantık programlama bağlamında Horn tümcelerinin model teorik özelliklerini araştırmış ve her kesin tümce kümesi D'nin benzersiz bir minimal model M'ye sahip olduğunu göstermiştir. Bir atomik formül A, ancak ve ancak A M'de doğruysa D tarafından mantıksal olarak ima edilir. Pozitif değişmezlerin varoluşsal olarak nicelenmiş bir birleşimiyle temsil edilen bir P problemi, ancak ve ancak P M'de doğruysa D tarafından mantıksal olarak ima edilir.
Önermesel Horn cümleleri hesaplama karmaşıklığı açısından da ilgi çekicidir, burada önermesel Horn cümlelerinin bir birleşimini doğru yapmak için doğruluk değeri atamalarını bulma problemi P-tamam bir problemdir (aslında doğrusal zamanda çözülebilir), bazen HORNSAT olarak adlandırılır. (Ancak kısıtlanmamış Boolean doyurulabilirlik problemi NP-tam bir problemdir). Birinci dereceden Horn cümlelerinin doğrulanabilirliği karar verilemez.