Horn cümlesi, değişmezlerden

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} $\neg p\lor \neg q\vee \cdots \vee \neg t\vee u$

fact: u {\displaystyle u} $u$

hedef maddesi: ¬ p ∨ ¬ q ∨ ⋯ ∨ ¬ t {\displaystyle \neg p\lor \neg q\vee \cdots \vee \neg t} $\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)} $\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))} $\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)). } $\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} $(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} $u$ , p {\displaystyle p} $p$ ve q {\displaystyle q} ve ⋯ {\displaystyle \cdots } göstermek için $\cdots$ ve show t {\displaystyle t} $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)} $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.

Sorular ve Yanıtlar

S: Horn cümlesi nedir?

C: 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.

S: Bunları ilk kim tanımladı?

C: Alfred Horn ilk olarak 1951 yılında bir makalesinde tanımlamıştır.

S: Belirli cümle nedir?

C: Tam olarak bir pozitif literal içeren bir Horn cümlesine belirli cümle denir.

S: Gerçek nedir?

C: Hiçbir olumsuz değişmezi olmayan bir kesin cümle bazen "olgu" olarak adlandırılır.

S: Amaç cümlesi nedir?

C: Olumlu bir değişmezi olmayan bir Horn cümlesi bazen bir hedef cümlesi olarak adlandırılır.

S: Önermesel olmayan durumlarda değişkenler nasıl çalışır?

C: Önermesel olmayan durumda, bir cümledeki tüm değişkenler, tüm cümlenin kapsamı ile dolaylı olarak evrensel olarak nicelenir. Bu, ifadenin her parçası için geçerli oldukları anlamına gelir.

S: Horn cümleleri yapıcı mantık ve hesaplamalı mantıkta nasıl bir rol oynar? C: Horn cümleleri birinci dereceden çözümleme ile otomatik teorem kanıtlamada önemli bir rol oynar çünkü iki Horn cümlesinin veya bir hedef ve bir kesin cümlenin çözümleyicisi, hedef cümlesinin olumsuzlaması olarak temsil edilen bir şeyi kanıtlarken daha fazla verimlilik yaratmak için kullanılabilir. Ayrıca Prolog gibi mantık programlama dilleri için temel olarak kullanılırlar ve burada hedef indirgeme prosedürleri gibi davranırlar.