हॉर्न क्लॉज
गणितीय तर्क और तर्क प्रोग्रामिंग में, एक हॉर्न क्लॉज एक विशेष नियम-जैसे फॉर्म का तार्किक सूत्र है जो इसे तर्क प्रोग्रामिंग, औपचारिक विनिर्देश और मॉडल सिद्धांत में उपयोग के लिए उपयोगी गुण प्रदान करता है। हॉर्न क्लॉज का नाम तर्कशास्त्री अल्फ्रेड हॉर्न के नाम पर रखा गया है, जिन्होंने पहली बार 1951 में उनके महत्व को इंगित किया था।[1]
परिभाषा
एक हॉर्न क्लॉज एक क्लॉज (तर्क) (शाब्दिक (गणितीय तर्क) का एक संयोजन) है जिसमें अधिकतम एक सकारात्मक, यानी निषेध, शाब्दिक है।
इसके विपरीत, अधिक से अधिक एक अस्वीकृत शाब्दिक के साथ शाब्दिक के संयोजन को दोहरे-हॉर्न क्लॉज कहा जाता है।
ठीक एक सकारात्मक शाब्दिक के साथ एक हॉर्न क्लॉज एक निश्चित क्लॉज या एक सख्त हॉर्न क्लॉज है;[2] एक निश्चित उपवाक्य जिसमें कोई नकारात्मक अक्षर नहीं है, एक इकाई उपवाक्य है,[3] और चर के बिना एक इकाई खंड एक तथ्य है;[4]. एक सकारात्मक शाब्दिक के बिना हॉर्न क्लॉज एक लक्ष्य क्लॉज है। ध्यान दें कि खाली खंड, जिसमें कोई अक्षर नहीं है (जो 'गलत के बराबर है) एक लक्ष्य खंड है। इन तीन प्रकार के हॉर्न क्लाजों को निम्नलिखित प्रस्ताव सूत्र उदाहरण में चित्रित किया गया है:
| Type of Horn clause | Disjunction form | Implication form | Read intuitively as |
|---|---|---|---|
| Definite clause | ¬p ∨ ¬q ∨ ... ∨ ¬t ∨ u | u ← p ∧ q ∧ ... ∧ t | assume that, if p and q and ... and t all hold, then also u holds |
| Fact | u | u ← true | assume that u holds |
| Goal clause | ¬p ∨ ¬q ∨ ... ∨ ¬t | false ← p ∧ q ∧ ... ∧ t | show that p and q and ... and t all hold[note 1] |
एक क्लॉज में सभी चर निहित रूप से सार्वभौमिक परिमाणीकरण हैं, जिसमें स्कोप संपूर्ण क्लॉज है। इस प्रकार, उदाहरण के लिए:
- ¬ मानव (एक्स) ∨ नश्वर (एक्स)
के लिए खड़ा है:
- ∀X( ¬ मानव(एक्स) ∨ प्राणघातक(एक्स) )
जो तार्किक रूप से इसके बराबर है:
- ∀X ( मानव (एक्स) → नश्वर (एक्स) )
महत्व
रचनात्मक तर्क और कम्प्यूटेशनल तर्क में हॉर्न क्लॉज एक बुनियादी भूमिका निभाते हैं। वे प्रथम-क्रम संकल्प द्वारा सिद्ध स्वचालित प्रमेय में महत्वपूर्ण हैं, क्योंकि दो हॉर्न खंडों का संकल्प (तर्क) स्वयं एक हॉर्न खंड है, और एक लक्ष्य खंड का संकल्प और एक निश्चित खंड एक लक्ष्य खंड है। हॉर्न क्लॉज के इन गुणों से एक प्रमेय को सिद्ध करने की अधिक दक्षता हो सकती है: लक्ष्य खंड इस प्रमेय का निषेध है; उपरोक्त तालिका में लक्ष्य खंड देखें। सहजता से, अगर हम φ साबित करना चाहते हैं, तो हम ¬φ (लक्ष्य) मान लेते हैं और जांचते हैं कि क्या ऐसी धारणा एक विरोधाभास की ओर ले जाती है। यदि ऐसा है, तो φ को धारण करना चाहिए। इस तरह, एक यांत्रिक साबित करने वाले उपकरण को दो सेटों (धारणाओं और (उप) लक्ष्यों) के बजाय केवल एक सेट के सूत्रों (धारणाओं) को बनाए रखने की आवश्यकता होती है।
कम्प्यूटेशनल जटिलता सिद्धांत में प्रस्तावित हॉर्न खंड भी रुचि रखते हैं। सत्य-मूल्य असाइनमेंट को खोजने की समस्या को हॉर्न-संतोषजनकता के रूप में जाना जाता है। यह समस्या पी-पूर्ण है और रैखिक समय में हल करने योग्य है।[5] ध्यान दें कि अप्रतिबंधित बूलियन संतुष्टि समस्या एक एनपी-पूर्ण समस्या है।
तर्क प्रोग्रामिंग
हॉर्न क्लॉज भी लॉजिक प्रोग्रामिंग का आधार हैं, जहां सामग्री सशर्त के रूप में निश्चित खंड लिखना आम है:
- (पी ∧ क्यू ∧ ... ∧ टी) → यू
वास्तव में, एक नए लक्ष्य खंड का निर्माण करने के लिए एक निश्चित खंड के साथ एक लक्ष्य खंड का संकल्प तर्क प्रोग्रामिंग भाषा प्रोलॉग के कार्यान्वयन में उपयोग किए जाने वाले एसएलडी संकल्प निष्कर्ष नियम का आधार है।
तर्क प्रोग्रामिंग में, एक निश्चित खंड लक्ष्य-घटाने की प्रक्रिया के रूप में व्यवहार करता है। उदाहरण के लिए, ऊपर लिखा हॉर्न क्लॉज प्रक्रिया के रूप में व्यवहार करता है:
- टू शो यू, शो पी एंड शो क्यू एंड ... और शो टी।
खंड के इस विपरीत उपयोग पर जोर देने के लिए, इसे अक्सर विपरीत रूप में लिखा जाता है:
- यू ← (पी ∧ क्यू ∧ ... ∧ टी)
प्रोलॉग में इसे इस प्रकार लिखा गया है:
u :- p, q, ..., t.
लॉजिक प्रोग्रामिंग में, संगणना और क्वेरी मूल्यांकन एक लक्ष्य खंड के रूप में हल की जाने वाली समस्या की अस्वीकृति का प्रतिनिधित्व करके किया जाता है। उदाहरण के लिए, सकारात्मक शाब्दिकों के अस्तित्वगत रूप से परिमाणित संयोजन को हल करने की समस्या:
- ∃X (p ∧ q ∧ ... ∧ t)
समस्या को अस्वीकार करके (इससे इनकार करते हुए कि इसका कोई समाधान है) प्रस्तुत किया जाता है, और लक्ष्य खंड के तार्किक रूप से समकक्ष रूप में इसका प्रतिनिधित्व किया जाता है:
- ∀X (गलत ← p ∧ q ∧ ... ∧ t)
प्रोलॉग में इसे इस प्रकार लिखा गया है:
:- p, q, ..., t.
समस्या को हल करना एक विरोधाभास को प्राप्त करने के बराबर है, जिसे खाली खंड (या गलत) द्वारा दर्शाया गया है। समस्या का समाधान लक्ष्य खंड में चर के लिए शर्तों का प्रतिस्थापन है, जिसे विरोधाभास के प्रमाण से निकाला जा सकता है। इस तरह से उपयोग किया जाता है, लक्ष्य खंड संबंधपरक डेटाबेस में संयोजन क्वेरी के समान होते हैं, और हॉर्न क्लॉज लॉजिक एक सार्वभौमिक ट्यूरिंग मशीन की कम्प्यूटेशनल शक्ति के बराबर है।
प्रस्तावना संकेतन वास्तव में अस्पष्ट है, और शब्द "लक्ष्य खंड" कभी-कभी अस्पष्ट रूप से भी प्रयोग किया जाता है। एक लक्ष्य खंड में चर को सार्वभौमिक या अस्तित्वगत रूप से परिमाणित के रूप में पढ़ा जा सकता है, और "झूठे" को व्युत्पन्न करने के रूप में व्याख्या की जा सकती है या तो एक विरोधाभास प्राप्त करने या हल करने के लिए समस्या का एक सफल समाधान प्राप्त करने के रूप में।[further explanation needed]
वैन एम्डेन और कोवाल्स्की (1976) ने लॉजिक प्रोग्रामिंग के संदर्भ में हॉर्न क्लॉज के मॉडल-सैद्धांतिक गुणों की जांच की, जिसमें दिखाया गया कि निश्चित क्लॉज डी के प्रत्येक सेट में एक अद्वितीय न्यूनतम मॉडल एम है। एक परमाणु सूत्र ए तार्किक रूप से डी द्वारा निहित है यदि और केवल यदि A, M में सत्य है। यह अनुसरण करता है कि एक समस्या P, जो सकारात्मक शाब्दिकों के एक अस्तित्वगत रूप से परिमाणित संयोजन द्वारा प्रस्तुत की जाती है, तार्किक रूप से D द्वारा निहित होती है यदि और केवल यदि P, M में सत्य है। हॉर्न क्लॉज का न्यूनतम मॉडल शब्दार्थ स्थिर के लिए आधार है तर्क कार्यक्रमों का मॉडल शब्दार्थ।[6]
टिप्पणियाँ
- ↑ Like in resolution theorem proving, "show φ" and "assume ¬φ" are synonymous (indirect proof); they both correspond to the same formula, viz. ¬φ.
यह भी देखें
संदर्भ
- ↑ Horn, Alfred (1951). "On sentences which are true of direct unions of algebras". Journal of Symbolic Logic. 16 (1): 14–21. doi:10.2307/2268661. JSTOR 2268661. S2CID 42534337.
- ↑ Makowsky (1987). "Why Horn Formulas Matter in Computer Science: Initial Structures and Generic Examples" (PDF). Journal of Computer and System Sciences. 34 (2–3): 266–292. doi:10.1016/0022-0000(87)90027-4.
- ↑ Buss, Samuel R. (1998). "An Introduction to Proof Theory". In Samuel R. Buss (ed.). प्रूफ थ्योरी की पुस्तिका. Studies in Logic and the Foundations of Mathematics. Vol. 137. Elsevier B.V. pp. 1–78. doi:10.1016/S0049-237X(98)80016-5. ISBN 978-0-444-89840-1. ISSN 0049-237X.
- ↑ Lau & Ornaghi (2004). "कम्प्यूटेशनल लॉजिक में सही प्रोग्राम डेवलपमेंट के लिए कंपोज़िशनल यूनिट्स निर्दिष्ट करना।". Lecture Notes in Computer Science. 3049: 1–29. doi:10.1007/978-3-540-25951-0_1. ISBN 978-3-540-22152-4.
- ↑ Dowling, William F.; Gallier, Jean H. (1984). "Linear-time algorithms for testing the satisfiability of propositional Horn formulae". Journal of Logic Programming. 1 (3): 267–284. doi:10.1016/0743-1066(84)90014-1.
- ↑ van Emden, M. H.; Kowalski, R. A. (1976). "The semantics of predicate logic as a programming language" (PDF). Journal of the ACM. 23 (4): 733–742. CiteSeerX 10.1.1.64.9246. doi:10.1145/321978.321991. S2CID 11048276.
