Horn cümlesi
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.
Tanım
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 ∨ ... ∨ ¬t ∨ u | u ← p ∧ q ∧ ... ∧ 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ış ← p ∧ q ∧ ... ∧ t | p ve q ve ... ve t terimlerinin hepsinin doğru olduğunu ispatlayınız |