हॉर्न क्लॉज
गणितीय तर्क और तर्क प्रोग्रामिंग में, हॉर्न क्लॉज एक विशेष नियम-जैसे प्ररूप का तार्किक सूत्र है जो इसे तर्क प्रोग्रामिंग, औपचारिक विनिर्देश और मॉडल सिद्धांत में उपयोग के लिए उपयोगी गुण प्रदान करता है। हॉर्न क्लॉज का नाम तर्कशास्त्री अल्फ्रेड हॉर्न के नाम पर रखा गया है, जिन्होंने पहली बार 1951 में उनके महत्व को इंगित किया था।[1]
परिभाषा
हॉर्न क्लॉज एक क्लॉज तर्क (अक्षर (गणितीय तर्क) का एक संयोजन) है जिसमें अधिकतम एक धनात्मक, अर्थात असंबद्ध, अक्षर (लिटेरल) है।
इसके विपरीत, अधिक से अधिक एक अस्वीकृत अक्षर के साथ अक्षर के संयोजन को दोहरे-हॉर्न क्लॉज कहा जाता है।
परिशुद्ध एक धनात्मक अक्षर के साथ एक हॉर्न क्लॉज एक निश्चित क्लॉज या एक विशुद्ध हॉर्न क्लॉज है;[2] बिना किसी नकारात्मक अक्षर के एक निश्चित क्लॉज एक यूनिट क्लॉज है,[3] और चर के बिना एक यूनिट क्लॉज एक तथ्य है;[4] धनात्मक अक्षर के बिना हॉर्न क्लॉज एक लक्ष्य क्लॉज है। ध्यान दें कि रिक्त क्लॉज, जिसमें कोई अक्षर नहीं है (जो असत्य के बराबर है) एक लक्ष्य क्लॉज है। इन तीन प्रकार के हॉर्न क्लाजों को निम्नलिखित प्रस्ताविक उदाहरण में चित्रित किया गया है:
| हॉर्न क्लॉज का प्रकार | वियोजन रूप | निहितार्थ रूप | सहज रूप से पढे |
|---|---|---|---|
| डेफिनिट क्लॉज | ¬p ∨ ¬q ∨ ... ∨ ¬t ∨ u | u ← p ∧ q ∧ ... ∧ t | मान लीजिए कि,
यदि p और q और ... और t सभी प्रग्रहण करते हैं, तो आप भी प्रग्रहण करते हैं |
| तथ्य | u | u ← true | मान लीजिए
तुम प्रग्रहण करते हो |
| लक्ष्य क्लॉज | ¬p ∨ ¬q ∨ ... ∨ ¬t | false ← p ∧ q ∧ ... ∧ t | बताते हैं कि
p और q और ... और t सभी प्रग्रहण करते हैं।[note 1] |
क्लॉज में सभी वेरिएबल्स को पूरी तरह से क्लॉज होने के विस्तार के साथ सार्वभौमिक रूप से परिमाणित किया गया है। इस प्रकार, उदाहरण के लिए:
- ¬ human(X) ∨ mortal(X) इसका अर्थ है:
- ∀X( ¬ human(X) ∨ mortal(X) ) जो तार्किक रूप से समतुल्य है:
- ∀X ( human(X) → mortal(X) )
महत्व
रचनात्मक तर्क और कम्प्यूटेशनल तर्क में हॉर्न क्लॉज एक मौलिक भूमिका निभाते हैं। वे प्रथम-क्रम वियोजन द्वारा सिद्ध स्वचालित प्रमेय में महत्वपूर्ण हैं, क्योंकि दो हॉर्न क्लॉज का वियोजन (तर्क) स्वयं एक हॉर्न क्लॉज है, और एक लक्ष्य क्लॉज का वियोजन और एक निश्चित क्लॉज एक लक्ष्य क्लॉज है। हॉर्न क्लॉज के इन गुणों से एक प्रमेय को सिद्ध करने की अधिक दक्षता हो सकती है: लक्ष्य क्लॉज इस प्रमेय का निषेध है; उपरोक्त सारणी में लक्ष्य क्लॉज देखें। सामान्य रूप से, यदि हम φ प्रमाणित करना चाहते हैं, तो हम ¬φ (लक्ष्य) मान लेते हैं और जांचते हैं कि क्या ऐसी धारणा एक विरोधाभास की ओर ले जाती है। यदि ऐसा है, तो φ को प्रग्रहण करना चाहिए। इस तरह, एक यांत्रिक प्रमाणित करने वाले उपकरण को दो सेटों (धारणाओं और (उप) लक्ष्यों) के अतिरिक्त केवल एक सेट के सूत्रों (धारणाओं) को बनाए रखने की आवश्यकता होती है।
कम्प्यूटेशनल जटिलता सिद्धांत में प्रस्तावित हॉर्न क्लॉज भी रुचि रखते हैं। सत्य-मान असाइनमेंट खोजने की समस्या को हॉर्नसैट के रूप में जाना जाता है। यह समस्या P-पूर्ण है और रैखिक समय में हल करने योग्य है।[5] ध्यान दें कि अप्रतिबंधित बूलियन संतुष्टि समस्या एक NP-पूर्ण समस्या है।
तर्क प्रोग्रामिंग
हॉर्न क्लॉज भी तार्किक प्रोग्रामिंग का आधार हैं, जहां सामग्री सशर्त के रूप में निश्चित क्लॉज लिखना सामान्य है:
- (p ∧ q ∧ ... ∧ t) → u
वास्तव में, नए लक्ष्य क्लॉज का निर्माण करने के लिए एक निश्चित क्लॉज के साथ एक लक्ष्य क्लॉज का वियोजन तर्क प्रोग्रामिंग भाषा प्रोलॉग के कार्यान्वयन में उपयोग किए जाने वाले एसएलडी वियोजन निष्कर्ष नियम का आधार है।
तर्क प्रोग्रामिंग में, एक निश्चित क्लॉज लक्ष्य-घटाने की प्रक्रिया के रूप में व्यवहार करता है। उदाहरण के लिए, ऊपर लिखा हॉर्न क्लॉज प्रक्रिया के रूप में व्यवहार करता है:
- to show u, show p and show q and ... and show t.
क्लॉज के इस विपरीत उपयोग पर महत्व देने के लिए, इसे प्रायः विपरीत रूप में लिखा जाता है:
- u ← (p ∧ q ∧ ... ∧ t)
प्रोलॉग में इसे इस प्रकार लिखा गया है:
u :- p, q, ..., t.
तार्किक प्रोग्रामिंग में, कम्प्यूटेशन और प्रश्न मूल्यांकन एक लक्ष्य क्लॉज के रूप में हल की जाने वाली समस्या की अस्वीकृति का प्रतिनिधित्व करके किया जाता है। उदाहरण के लिए, धनात्मक अक्षरो के अस्तित्वगत रूप से परिमाणित संयोजन को हल करने की समस्या:
- ∃X (p ∧ q ∧ ... ∧ t)
समस्या को अस्वीकार करके (इससे अस्वीकृत करते हुए कि इसका कोई समाधान है) प्रस्तुत किया जाता है, और लक्ष्य क्लॉज के तार्किक रूप से समकक्ष रूप में इसका प्रतिनिधित्व किया जाता है:
- ∀X (false ← p ∧ q ∧ ... ∧ t)
प्रोलॉग में इसे इस प्रकार लिखा गया है:
:- p, q, ..., t.
समस्या को हल करना एक विरोधाभास (कंट्राडिक्शन) को प्राप्त करने के बराबर है, जिसे रिक्त क्लॉज (या गलत) द्वारा दर्शाया गया है। समस्या का समाधान लक्ष्य क्लॉज में चर के लिए शर्तों का प्रतिस्थापन है, जिसे विरोधाभास के प्रमाण से निकाला जा सकता है। इस तरह से उपयोग किया जाता है, लक्ष्य क्लॉज संबंधपरक डेटाबेस में संयोजन प्रश्न के समान होते हैं, और हॉर्न क्लॉज तार्किक एक सार्वभौमिक ट्यूरिंग मशीन की कम्प्यूटेशनल क्षमता के समान है।
प्रस्तावना संकेतन वास्तव में अस्पष्ट है, और शब्द "लक्ष्य क्लॉज" कभी-कभी अस्पष्ट रूप से भी प्रयोग किया जाता है। एक लक्ष्य क्लॉज में चर को सार्वभौमिक या अस्तित्वगत रूप से परिमाणित के रूप में पढ़ा जा सकता है, और "असत्य" को व्युत्पन्न करने के रूप में व्याख्या की जा सकती है या तो एक विरोधाभास प्राप्त करने या हल करने के लिए समस्या का एक सफल समाधान प्राप्त करने के रूप में की जाती है।[further explanation needed]
वैन एम्डेन और कोवाल्स्की (1976) ने तार्किक प्रोग्रामिंग के संदर्भ में हॉर्न क्लॉज के मॉडल-सैद्धांतिक गुणों की जांच की, जिसमें दिखाया गया कि निश्चित क्लॉज D के प्रत्येक सेट में एक अद्वितीय न्यूनतम मॉडल M है। एक परमाणु सूत्र A तार्किक रूप से D द्वारा निहित है यदि और केवल यदि 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.
