İçeriğe atla

Horn cümlesi

Vikipedi, özgür ansiklopedi

Matematiksel mantık ve mantık programlamada, kural gibi özel bir biçime sahip mantıksal formüllere Horn cümlesi denir. Bu özel biçim mantık programlama, kurallı belirtim ve modeller kuramı konularında kullanışlıdır. Horn cümlelerinin önemini 1951'de ortaya koyan mantıkçı Alfred Horn bu kavramın isim babası olmuştur.

Bir Horn cümlesi en fazla bir olumlu (yani olumsuzlanmamış) terimden oluşan bir cümledir (ayrılma (v) bağlacı ile bağlanmış terim kümesi).

Buna karşın, ayrılma (v) bağlacı ile bağlanmış sözcükler eğer en fazla bir olumsuz sözcüğe sahipse çiftli-Horn cümlesi olarak adlandırılır.

Sadece bir olumlu terime sahip olan Horn cümlesine belirli cümle denir; hiç olumsuz terime sahip olmayan belirli cümlelere olgu denir; olumlu terimi olmayan Horn cümleleri amaç cümlesi olarak da adlandırılır (hiçbir terim içermeyen boş bir cümle de bir amaç cümlesidir). Horn cümlelerinin bu üç çeşidi aşağıdaki tabloda gösterilmiştir:

Ayrılma biçimi
Gerektirme biçimi
Anlamı
Belirli cümle ¬p ∨ ¬q ∨ ... ∨ ¬tu upq ∧ ... ∧ t eğer p ve q ve ... ve t terimlerinin hepsi doğruysa, o zaman u da doğrudur
Olgu u u u doğrudur
Amaç cümlesi ¬p ∨ ¬q ∨ ... ∨ ¬t yanlış ← pq ∧ ... ∧ t p ve q ve ... ve t terimlerinin hepsinin doğru olduğunu ispatlayınız