Korna cümlesi - Horn clause
Olarak matematiksel mantık ve mantık programlama , bir Horn cümlesi o mantık programlama, kullanım için yararlı özellikleri veren belirli kural-benzeri formda bir mantıksal formül resmi tarifname ve örnek teorisi . Horn cümleleri, 1951'de önemine ilk kez dikkat çeken mantıkçı Alfred Horn'un adını almıştır .
Tanım
Boynuzu maddesi a, maddesi (bir ayrılma bölgesinin değişmez en az bir pozitif, diğer bir deyişle) unnegated , değişmez.
Tersine, değişmezlerin en fazla bir olumsuzlanmış değişmezle ayrılmasına dual-Horn yan tümcesi denir .
Tam olarak bir pozitif değişmezi olan bir Horn yan tümcesi, kesin bir yan tümce veya katı bir Horn yan tümcesidir ; olumsuz değişmezleri olmayan belirli bir madde, bir birim maddesidir ve değişkenleri olmayan bir birim maddesi bir olgudur ; Olumlu bir değişmezi olmayan bir Horn yan tümcesi, bir hedef yan tümcesidir . Hiçbir hazır bilgi içermeyen boş yan tümcenin ( false 'a eşdeğerdir ) bir hedef yan tümcesi olduğuna dikkat edin. Bu üç tür Horn cümlesi aşağıdaki önerme örneğinde gösterilmiştir:
| Horn cümlesinin türü | ayırma formu | ima formu | Sezgisel olarak oku |
|---|---|---|---|
| kesin cümle | ¬ p ∨ ¬ q ∨ ... ∨ ¬ t ∨ u | u ← p ∧ q ∧ ... ∧ t | p ve q ve ... ve t'nin tümü geçerliyse , u'nun da geçerli olduğunu varsayalım |
| gerçek | sen | sen ← doğru | varsayalım u tutan |
| hedef maddesi | ¬ p ∨ ¬ q ∨ ... ∨ ¬ t | yanlış ← p ∧ q ∧ ... ∧ t | olduğunu göstermektedir p ve q ve ... ve t bütün tutun |
Bir yan tümcedeki tüm değişkenler , kapsam tüm yan tümceyi oluşturacak şekilde örtük olarak evrensel olarak nicelenir . Böylece, örneğin:
- ¬ insan ( X ) ∨ ölümlü ( X )
şu anlama gelir:
- ∀X( ¬ insan ( X ) ∨ ölümlü ( X ) )
hangi mantıksal olarak eşdeğerdir:
- ∀X ( insan ( X ) → ölümlü ( X ) )
Önemi
Boynuz cümleleri, yapıcı mantık ve hesaplama mantığında temel bir rol oynar . Bunlar önemli olan kanıtlayan otomatik teoremi ile birinci dereceden çözünürlüğü nedeniyle, resolvent iki Horn maddelerinin bir Horn cümlesi kendisidir ve bir hedef maddesi rezolventi ve kesin bir hüküm kale deyimdir. Boynuz tümcelerinin bu özellikleri, bir teoremi kanıtlamada daha fazla etkinliğe yol açabilir: hedef yan tümcesi bu teoremin olumsuzlanmasıdır; yukarıdaki tablodaki Hedef maddesine bakın . Sezgisel olarak, eğer φ'yi ispatlamak istersek, ¬φ (hedef) olduğunu varsayarız ve bu varsayımın bir çelişkiye yol açıp açmadığını kontrol ederiz. Eğer öyleyse, o zaman φ tutmalıdır. Bu şekilde, bir mekanik kanıtlama aracının, iki takım (varsayımlar ve (alt) hedefler) yerine yalnızca bir formül takımı (varsayımlar) sağlaması gerekir.
Önerme Boynuzu tümceleri, hesaplama karmaşıklığıyla da ilgilenir . Önerme Horn cümlelerinin bir birleşimini doğru yapmak için doğruluk değeri atamalarını bulma sorunu HORNSAT olarak bilinir . Bu problem P-tam ve lineer zamanda çözülebilir . Sınırsız unutmayın Boole Satisfiability sorun bir olan NP-tam problemi.
mantık programlama
Boynuz cümleleri, aynı zamanda, belirli cümleleri bir ima şeklinde yazmanın yaygın olduğu mantıksal programlamanın temelidir :
- ( p ∧ q ∧ ... ∧ t ) → u
Aslında, yeni bir hedef cümlesi üretmek için belirli bir cümle ile bir hedef cümlesinin çözümü , mantık programlama dili Prolog'un uygulanmasında kullanılan SLD çözünürlük çıkarım kuralının temelidir .
Mantıksal programlamada, belirli bir yan tümce, bir hedef azaltma prosedürü gibi davranır. Örneğin, yukarıda yazılan Horn yan tümcesi, prosedür gibi davranır:
- göstermek için u , gösteri p ve gösteri q ve ... ve gösteri t .
Cümlenin bu ters kullanımını vurgulamak için, genellikle ters biçimde yazılır:
- u ← ( p ∧ q ∧ ... ∧ t )
In Prolog bu şekilde yazılır:
u :- p, q, ..., t.
Mantıksal programlamada, çözülecek bir problemin olumsuzlanması bir amaç cümlesi olarak temsil edilerek hesaplama ve sorgu değerlendirmesi yapılır. Örneğin, pozitif değişmezlerin varoluşsal olarak nicelleştirilmiş birleşimini çözme sorunu:
- ∃ X ( p ∧ q ∧ ... ∧ t )
problemi olumsuzlayarak (bir çözümü olduğunu inkar ederek) ve onu mantıksal olarak eşdeğer bir hedef cümlesi biçiminde temsil ederek temsil edilir:
- ∀ X ( yanlış ← p ∧ q ∧ ... ∧ t )
In Prolog bu şekilde yazılır:
:- p, q, ..., t.
Sorunu çözmek, boş yan tümce (veya "yanlış") ile temsil edilen bir çelişki türetmek anlamına gelir. Problemin çözümü, çelişki ispatından çıkarılabilen, amaç cümlesindeki değişkenler için terimlerin ikame edilmesidir. Bu şekilde kullanıldığında, hedef cümleleri ilişkisel veritabanlarındaki birleşik sorgulara benzer ve Horn cümlesi mantığı, evrensel bir Turing makinesinin hesaplama gücüyle eşdeğerdir .
Prolog gösterimi aslında belirsizdir ve "hedef tümcesi" terimi bazen belirsiz bir şekilde kullanılır. Bir amaç tümcesindeki değişkenler evrensel veya varoluşsal olarak nicel olarak okunabilir ve “yanlış” türetme, ya bir çelişki türetme ya da çözülecek problemin başarılı bir çözümünü türetme olarak yorumlanabilir.
Van Emden ve Kowalski (1976), Horn yan tümcelerinin model-teorik özelliklerini mantık programlaması bağlamında araştırdı ve her kesin tümce kümesinin D benzersiz bir minimum M modeline sahip olduğunu gösterdi . Bir atom formülü A , mantıksal olarak D tarafından ima edilir, ancak ve ancak M'de A doğruysa . Bundan , pozitif değişmezlerin varoluşsal olarak nicelleştirilmiş bir birleşimiyle temsil edilen bir P sorununun , yalnızca ve ancak P , M'de doğruysa , mantıksal olarak D tarafından ima edildiği sonucu çıkar . Horn cümlelerinin minimal model semantiği , mantık programlarının kararlı model semantiğinin temelidir .