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