एकीकरण (कंप्यूटर विज्ञान): Difference between revisions

Latest revision as of 11:05, 12 August 2023

लॉजिक और कंप्यूटर विज्ञान में एकीकरण सिंबॉलिक अभिव्यक्तियों (गणित) के बीच समीकरणों को हल करने के लिए कलन विधि प्रक्रिया का उपयोग किया जाता है। उदाहरण के लिए x,y,z को चर के रूप में उपयोग करते हुए एकल समीकरण समुच्चय { cons(x,cons(x,nil)) = cons(2,y) } एक वाक्यात्मक प्रथम-क्रम एकीकरण समस्या के रूप में है, जिसके पास प्रतिस्थापन {x ↦ 2, y ↦ cons(2,nil) } के रूप में एकमात्र हल होता है।

एकीकरण कलन विधि की खोज सबसे पहले जैक्स हेरब्रांड ने की थी,^[1]^[2]^[3] जबकि पहली फॉर्मल जांच का श्रेय जॉन एलन रॉबिन्सन को दिया जाता है,^[4]^[5] जिन्होंने प्रथम-क्रम लॉजिक के लिए अपने हल प्रक्रिया के मौलिक निर्माण खंड के रूप में प्रथम-क्रम वाक्यात्मक एकीकरण का उपयोग किया है, इस प्रकार स्वचालित लॉजिक को प्रौद्योगिकी में एक बड़े कदम के रूप में माना जाता है, क्योंकि इसने संयोजन विस्फोट के एक स्रोत को समाप्त कर दिया था। यह संयोजक के रूप में आज भी एक स्रोत बन गया है और इसे स्वचालित लॉजिक एकीकरण का मुख्य क्षेत्र माना जाता है। वाक्यात्मक प्रथम-क्रम एकीकरण का उपयोग लॉजिक प्रोग्रामिंग और प्रोग्रामिंग लैंग्वेज टाइप प्रणाली कार्यान्वयन के रूप में किया जाता है और इस प्रकार विशेष रूप से हिंडले-मिलनर आधारित टाइप अनुमान कलन विधि के रूप में होता है। सिमेंटिक एकीकरण का उपयोग एसएमटी सॉल्वर्स, शब्द पुनर्लेखन कलन विधि और क्रिप्टोआलेख़िक प्रोटोकॉल विश्लेषण के रूप में किया जाता है। उच्च-क्रम एकीकरण का उपयोग प्रूफ़ सहायकों के रूप में किया जाता है। उदाहरण के लिए इसाबेल और ट्वेल्व और उच्च-क्रम एकीकरण के प्रतिबंधित रूपों का उपयोग कुछ प्रोग्रामिंग लैंग्वेज कार्यान्वयन के रूप में किया जाता है, चूकि कुछ प्रोग्रामिंग लैम्डैप्रोलॉग के सीमित रूपों का उपयोग किया जाता है, क्योंकि उच्च-क्रम पैटर्न इक्स्प्रेसिव के रूप में होते हैं, फिर भी उनकी संबद्ध एकीकरण प्रक्रिया सैद्धांतिक गुणों को प्रथम-क्रम एकीकरण के रूप में निकटता बनाए रखती है।

फॉर्मल परिभाषा

एकीकरण समस्या हल करने के लिए समीकरणों का एक सीमित समुच्चय $E ={l 1 ≐ r 1, ..., l n ≐ r n}$ के रूप में होता है, जहाँ $l i, r i$ पदों या अभिव्यक्तियों के समुच्चय $T$ के रूप में होता हैं। समीकरण समुच्चय या एकीकरण समस्या में किन अभिव्यक्तियों या शब्दों को घटित होने की अनुमति होती है और किन अभिव्यक्तियों को समान माना जाता है, इसके आधार पर एकीकरण के रूप में कई ढांचे प्रतिष्ठित हैं। यदि उच्च-क्रम वाले चर अर्थात फलन (गणित) का प्रतिनिधित्व करने वाले चर को एक अभिव्यक्तियों में अनुमति होती है, तो प्रक्रिया को 'उच्च-क्रम एकीकरण' कहा जाता है। अन्यथा 'प्रथम-क्रम एकीकरण' का रूप कहा जाता है। यदि प्रत्येक समीकरण के दोनों पक्षों को वस्तुतः समान बनाने के लिए किसी समाधान की आवश्यकता होती है, तो प्रक्रिया को 'वाक्यविन्यास' या 'मुक्त एकीकरण' कहा जाता है, अन्यथा सिमेंटिक या 'समीकरणात्मक एकीकरण या ई- एकीकरण या एकीकरण मॉड्यूलो सिद्धांत कहा जाता है।

प्रिरेक्विज़िट

औपचारिक रूप से एक एकीकरण दृष्टिकोण का अनुमान लगाया जाता है

एक अनंत समुच्चय $V$ चर का. उच्च-क्रम एकीकरण के लिए, इसे चुनना सुविधाजनक है $V$ लैम्ब्डा-टर्म बाध्य चर के समुच्चय से भिन्न हो जाता है।
एक समुच्चय $T$ ऐसे शब्दों का $V\subseteq T$ . प्रथम-क्रम एकीकरण के लिए, $T$ सामान्यतः प्रथम-क्रम शब्दों चर और फलन प्रतीकों से निर्मित शब्द का समुच्चय होता है। उच्च-क्रम एकीकरण के लिए $T$ इसमें प्रथम-क्रम वाले शब्द और लैम्ब्डा शब्द कुछ उच्च-क्रम वाले चर वाले शब्द के रूप में सम्मिलित होते हैं।
एक मैपिंग संस्करण: $T\rightarrow$ पावर समुच्चय | $\mathbb {P}$ $(V)$ , प्रत्येक पद को निर्दिष्ट करना $t$ समुच्चय ${\text{vars}}(t)\subsetneq V$ में होने वाले मुक्त चर के रूप में $t$ होता है.
एक सिद्धांत या तुल्यता संबंध $\equiv$ पर $T$ , यह दर्शाता है, कि कौन से पद समान माने जाते हैं। प्रथम-क्रम ई- एकीकरण के लिए, $\equiv$ कुछ फलन प्रतीकों के बारे में पृष्ठभूमि ज्ञान को दर्शाता है; उदाहरण के लिए, यदि $\oplus$ क्रमविनिमेय माना जाता है, $t\equiv u$ यदि $u$ वहां से परिणाम मिले $t$ के लॉजिक की अदला-बदली करके $\oplus$ कुछ संभवतः सभी घटनाओं पर। ^{[note 1]} सबसे विशिष्ट स्थिति में जब कोई पृष्ठभूमि ज्ञान नहीं होता है, तो मात्र शाब्दिक रूप से या वाक्यात्मकरूप से समान शब्दों को समान माना जाता है। इस स्थिति में ≡ को मुक्त सिद्धांत कहा जाता है, क्योंकि यह एक स्वतंत्र वस्तु के रूप में है, खाली सिद्धांत क्योंकि समीकरण वाक्य (गणितीय लॉजिक ) का समुच्चय या पृष्ठभूमि ज्ञान के रूप में खाली है, अव्याख्यायित फलन के सिद्धांत पर किया जाता है, क्योंकि एकीकरण अनिर्वचनीय शब्द (लॉजिक)) या बीजगणितीय विनिर्देश के सिद्धांत के रूप में किया जाता है, क्योंकि सभी फलन प्रतीक मात्र उन पर काम करने के अतिरिक्त डेटा शब्द के रूप में जाने जाते है। सामान्यतः उच्च-क्रम एकीकरण के लिए $t\equiv u$ यदि $t$ और $u$ अल्फ़ा समतुल्य होता है.

शब्दों और सिद्धांत का समुच्चय समाधानों के समुच्चय को कैसे प्रभावित करता है, इसके उदाहरण के रूप में वाक्यात्मक प्रथम-क्रम एकीकरण समस्या { y = cons(2,y) } का परिमित शब्दों के समुच्चय पर कोई हल नहीं है। चूंकि, ट्री समुच्चय सिद्धांत शर्तों के समुच्चय पर इसका एकल हल के रूप में { y ↦ cons(2,cons(2,cons(2,...)) } होता है। इसी प्रकार सिमेंटिक प्रथम-क्रम एकीकरण समस्या { a⋅x = x⋅a } में फॉर्म का प्रत्येक प्रतिस्थापन { x ↦ a⋅...⋅a } एक अर्धसमूह में हल के रूप में होता है, अर्थात यदि (⋅) को साहचर्य माना जाता है, लेकिन वही समस्या जिसे एबेलियन समूह में देखा जाता है, जहां (⋅) को क्रमविनिमेय के रूप में माना जाता है और इस प्रकार हल के रूप में कोई भी प्रतिस्थापन होता है

उच्च-क्रम एकीकरण के उदाहरण के रूप में एकल समुच्चय { a = y(x) } एक वाक्यात्मक दूसरे क्रम की एकीकरण समस्या के रूप में होता है, क्योंकि y एक फलन चर है। एक हल x ↦ a, y ↦ आइडेंटिटी फलन) } है, इस प्रकार दूसरा { y ↦ निरंतर फलन है, जो प्रत्येक मान को a, x ↦ को किसी भी मान पर मैप करता है।

प्रतिस्थापन

प्रतिस्थापन एक मानचित्रण है $\sigma :V\rightarrow T$ चर से पदों तक; संकेतन $\{x_{1}\mapsto t_{1},...,x_{k}\mapsto t_{k}\}$ प्रत्येक चर के रूप में प्रतिस्थापन मानचित्रण को संदर्भित करता है $x_{i}$ पद के लिए $t_{i}$ , के लिए $i=1,...,k$ , और प्रत्येक अन्य चर स्वयं के लिए होता है। उस प्रतिस्थापन को किसी पद पर प्रयुक्त करना $t$ उपसर्ग संकेतन में इस प्रकार लिखा गया है $t\{x_{1}\mapsto t_{1},...,x_{k}\mapsto t_{k}\}$ ; इसका अर्थ है (एक साथ) प्रत्येक चर की प्रत्येक घटना को प्रतिस्थापित करना $x_{i}$ अवधि में $t$ द्वारा $t_{i}$ . के रूप में होता है और इस प्रकार किसी पद $t$ .में प्रतिस्थापन $t\tau$ प्रयुक्त करने का परिणाम $\tau$ उस पद पद के लिए $t$ का उदाहरण कहलाता है। प्रथम-क्रम उदाहरण के रूप में प्रतिस्थापन ${x \mapsto h (a, y), z \mapsto b}$ प्रयुक्त शब्द के लिए होता है.

	$f($	${\textbf {x}}$	$,a,g($	${\textbf {z}}$	$),y)$
प्रतिफल
	$f($	${\textbf {h}}({\textbf {a}},{\textbf {y}})$	$,a,g($	${\textbf {b}}$	$),y).$

सामान्यीकरण, विशेषज्ञता

यदि एक शब्द $t$ एक पद के समतुल्य एक उदाहरण है $u$ , अर्थात्, यदि $t\sigma \equiv u$ कुछ प्रतिस्थापन के लिए $\sigma$ , तब $t$ से अधिक सामान्य कहा जाता है $u$ , और $u$ से अधिक विशेष कहा जाता है या उसमें सम्मिलित किया जाता है, $t$ . उदाहरण के लिए, $x\oplus a$ से अधिक सामान्य है $a\oplus b$ यदि ⊕ क्रमविनिमेय x, के रूप में है तब $(x\oplus a)\{x\mapsto b\}=b\oplus a\equiv a\oplus b$ .गुणधर्म है

यदि ≡ शब्दों की शाब्दिक वाक्यविन्यास के रूप में पहचान है, तो एक शब्द दूसरे की तुलना में अधिक सामान्य और अधिक विशेष दोनों हो सकते है, यदि दोनों शब्द मात्र उनके परिवर्तनीय नामों में भिन्न हों न कि उनकी वाक्यात्मक संरचना में ऐसे शब्दों को परिवर्त या एक-दूसरे का नाम बदलना कहा जाता है।

उदाहरण के लिए,

 $f(x_{1},a,g(z_{1}),y_{1})$

का एक प्रकार होता है

 $f(x_{2},a,g(z_{2}),y_{2})$ ,

जब से

f(x_{1},a,g(z_{1}),y_{1})\{x_{1}\mapsto x_{2},y_{1}\mapsto y_{2},z_{1}\mapsto z_{2}\}=f(x_{2},a,g(z_{2}),y_{2})

और

f(x_{2},a,g(z_{2}),y_{2})\{x_{2}\mapsto x_{1},y_{2}\mapsto y_{1},z_{2}\mapsto z_{1}\}=f(x_{1},a,g(z_{1}),y_{1}).

चूंकि,

f(x_{1},a,g(z_{1}),y_{1})

का एक प्रकार नहीं है

f(x_{2},a,g(x_{2}),x_{2})

, क्योंकि कोई भी प्रतिस्थापन पश्चात वाले पद को पहले वाले में नहीं बदल सकता है।

इसलिए पश्चात वाला शब्द पहले वाले की तुलना में उचित रूप से अधिक विशेष होता है।

यादृच्छिक के लिए $\equiv$ , एक शब्द संरचनात्मक रूप से भिन्न शब्द की तुलना में अधिक सामान्य और अधिक विशेष दोनों हो सकता है।

उदाहरण के लिए, यदि ⊕ निष्क्रिय है, अर्थात यदि सदैव $x\oplus x\equiv x$ , फिर पद $x\oplus y$ से अधिक सामान्य है $z$ ,^{[note 2]} और इसके विपरीत,^{[note 3]} यद्यपि $x\oplus y$ और $z$ भिन्न-भिन्न संरचना के हैं.

एक प्रतिस्थापन $\sigma$ प्रतिस्थापन से अधिक विशेष होता है या उसमें सम्मिलित होता है $\tau$ यदि $t\sigma$ द्वारा सम्मिलित किया गया है $t\tau$ प्रत्येक पद के लिए $t$ . हम भी यही कहते हैं $\tau$ से अधिक सामान्य है $\sigma$ . अधिक फॉर्मल रूप से एक गैर-रिक्त अनंत समुच्चय लें $V$ सहायक चर जैसे कि को E समीकरण नहीं $l_{i}\doteq r_{i}$ एकीकरण समस्या में चर के रूप में सम्मिलित हैं $V$ . फिर एक प्रतिस्थापन $\sigma$ किसी अन्य प्रतिस्थापन द्वारा सम्मिलित किया गया है $\tau$ यदि कोई प्रतिस्थापन है $\theta$ ऐसा कि सभी शर्तों के लिए $X\notin V$ , $X\sigma \equiv X\tau \theta$ .^[6]उदाहरण के लिए $\{x\mapsto a,y\mapsto a\}$ द्वारा सम्मिलित किया गया है $\tau =\{x\mapsto y\}$ , का उपयोग करना $\theta =\{y\mapsto a\}$ , लेकिन

 $\sigma =\{x\mapsto a\}$  में सम्मिलित नहीं है  $\tau =\{x\mapsto y\}$ , जैसा  $f(x,y)\sigma =f(a,y)$  का उदाहरण नहीं है

$f(x,y)\tau =f(y,y)$ .^[7]}} के रूप में होता है.

हल समुच्चय

एक प्रतिस्थापन σ एकीकरण समस्या E के रूप में एक हल है यदि $l i σ \equiv r i σ$ के लिए $i=1,...,n$ . ऐसे प्रतिस्थापन को E का एकीकरण कर्ता भी कहा जाता है।

उदाहरण के लिए, यदि ⊕ साहचर्य है, तो एकीकरण समस्या {x ⊕ a ≐ a ⊕ x } के हल हैं {x ↦ a' '}, {x ↦ a ⊕ a}, {x ↦ a ⊕ a ⊕ a}, आदि ,जबकि समस्या { x ⊕ a ≐ a } का कोई हल नहीं होता है।

दी गई एकीकरण समस्या E के लिए, एकीकरण कर्ताओं के एक समुच्चय S को पूर्ण कहा जाता है यदि प्रत्येक हल प्रतिस्थापन को एस में कुछ प्रतिस्थापन द्वारा समाहित किया जाता है। एक पूर्ण प्रतिस्थापन समुच्चय निरंतर उपलब्ध होता है, उदाहरण के लिए सभी समाधानों का समुच्चय लेकिन कुछ रूप रेखाओं में जैसे कि अप्रतिबंधित उच्च-क्रम एकीकरण में यह निर्धारित करने की समस्या होती है, कि क्या पूर्ण प्रतिस्थापन समुच्चय गैर रिक्त अनिर्णीत रूप में होता है।

समुच्चय S को न्यूनतम कहा जाता है, इसका कोई भी सदस्य दूसरे को सम्मिलित नहीं करता है। इस प्रकार रूपरेखा के आधार पर एक पूर्ण और न्यूनतम प्रतिस्थापन समुच्चय में शून्य एक परिमित रूप से कई या अनंत रूप से कई सदस्य होते हैं या अनावश्यक सदस्यों की अनंत श्रृंखला के कारण पूर्ण रूप में उपलब्ध नहीं होते हैं।^[8] इस प्रकार सामान्यतः एकीकरण कलन विधि पूर्ण समुच्चय के एक सीमित सन्निकटन की गणना करते हैं, जो न्यूनतम रूप में हो भी सकता है और नहीं भी हो सकता है, चूंकि अधिकांश कलन विधि जब संभव होता है तो निरर्थक एकीकरण कर्ताओं से बचते हैं।^[6] प्रथम-क्रम वाक्यात्मक एकीकरण के लिए, मार्टेली और मोंटानारी^[9] एक कलन विधि को दिया जाता है, जो अघुलनशीलता की रिपोर्ट करता है या एकल यूनिफायर की गणना करता है, जो स्वयं एक पूर्ण और न्यूनतम प्रतिस्थापन समुच्चय के रूप में बनाता है, जिसे सबसे सामान्य यूनिफायर कहा जाता है।

प्रथम-क्रम शब्दों का वाक्यात्मकएकीकरण

प्रतिस्थापन σ द्वारा टर्म t1 और t2 को वाक्यात्मकरूप से एकीकृत करने का योजनाबद्ध त्रिभुज आरेख है

प्रथम-क्रम शब्दों का वाक्यात्मक एकीकरण सबसे व्यापक रूप से उपयोग किया जाने वाला एकीकरण ढांचा है।

यह प्रथम-क्रम के पदों के समुच्चय T के रूप में आधारित है, (चरों के कुछ दिए गए समुच्चय V, स्थिरांकों के C और F पर)_n n-ary फलन प्रतीकों का और ≡ वाक्यात्मक समानता पर आधारित है।

इस ढांचे में, प्रत्येक हल योग्य एकीकरण समस्या ${l 1 ≐ r 1, ..., l n ≐ r n}$ के पास पूर्ण, और स्पष्ट रूप से न्यूनतम, एकल (गणित) हल समुच्चय है ${σ}$ .

इसके सदस्य $σ$ को समस्या का सबसे सामान्य एकीकरणकर्ता (एमजीयू) का रूप कहा जाता है।

जब एमजीयू प्रयुक्त किया जाता है तो प्रत्येक संभावित समीकरण के बायीं और दायीं ओर के पद वाक्यात्मक रूप से समतुल्य हो जाते हैं। $l 1 σ = r 1 σ \land ... \land l n σ = r n σ$ .

समस्या का कोई भी एकीकरणकर्ता समाहित हो जाता है^{[note 4]} एमजीयू द्वारा $σ$ .

एमजीयू वेरिएंट तक अद्वितीय है: यदि एस₁ और एस₂ दोनों एक ही वाक्यात्मक एकीकरण समस्या के पूर्ण और न्यूनतम हल समुच्चय हैं, तो S₁ = { σ₁ } और S₂ = { σ₂ } कुछ प्रतिस्थापनों के लिए $σ 1$ और $σ 2,$ और $xσ 1$ का एक प्रकार है $xσ 2$ समस्या में आने वाले प्रत्येक चर x के लिए है।

उदाहरण के लिए, एकीकरण समस्या { x ≐ z, y ≐ f(x) } में एक एकीकृतकर्ता है { x ↦ z, y ↦ f(z) }, क्योंकि

x	{ x ↦ z, y ↦ f(z) }	=	z	=	z	{ x ↦ z, y ↦ f(z) }	, and
y	{ x ↦ z, y ↦ f(z) }	=	f(z)	=	f(x)	{ x ↦ z, y ↦ f(z) }	.

यह सबसे सामान्य एकीकरणकर्ता के रूप में है

समान समस्या के लिए अन्य एकीकरणकर्ता हैं, उदा. { x ↦ f(x₁), y ↦ f(f(x₁)), z ↦ f(x₁) }, { x ↦ f(f(x₁)), y ↦ f(f(f(x₁))), z ↦ f(f(x₁)) }, और इसी प्रकार ऐसे अपरिमित रूप से अनेक एकीकरण कर्ता के रूप में हैं।

एक अन्य उदाहरण के रूप में समस्या g(x,x) ≐ f(y) का शाब्दिक पहचान होने के संबंध में कोई हल नहीं है, क्योंकि बाएं और दाएं तरफ प्रयुक्त कोई भी प्रतिस्थापन क्रमशः सबसे बाहरी g और f को बनाए रखेगा, और विभिन्न बाहरीतम फलन प्रतीकों वाले शब्द वाक्यात्मक रूप से भिन्न होते हैं।

एक एकीकरण कलन विधि

Robinson's 1965 unification algorithm

Symbols are ordered such that variables precede function symbols. Terms are ordered by increasing written length; equally long terms are ordered lexicographically.^[10] For a set T of terms, its disagreement path p is the lexicographically least path where two member terms of T differ. Its disagreement set is the set of subterms starting at p, formally: $t\in T$ }.^[11]
Algorithm:^[12] Given a set T of terms to be unified Let $\sigma$ initially be the identity substitution do forever if $T\sigma$ is a singleton set then return $\sigma$ fi let D be the disagreement set of $T\sigma$ let s, t be the two lexicographically least terms in D if s is not a variable or s occurs in t then return "NONUNIFIABLE" fi $\sigma :=\sigma \{s\mapsto t\}$ done

रॉबिन्सन (1965) द्वारा दिया गया पहला कलन विधि अधिक अप्रभावी था; cf डिब्बा।

निम्नलिखित तेज़ कलन विधि की उत्पत्ति मार्टेली, मोंटानारी (1982) के रूप में हुई थी।^{[note 5]}

यह पेपर एक कुशल वाक्यात्मक एकीकरण कलन विधि खोजने के पिछले प्रयासों को भी सूचीबद्ध करता है,^[13]^[14]^[15]^[16]^[17]^[18] और बताता है, कि रैखिक-समय कलन विधि की खोज मार्टेली, मोंटानारी (1976) द्वारा स्वतंत्र रूप से की गई थी।^[15]और पैटरसन, वेगमैन (1976,^[19] 1978^[16]).^{[note 6]} का रूप होता है.

एक परिमित समुच्चय दिया गया है $G=\{s_{1}\doteq t_{1},...,s_{n}\doteq t_{n}\}$ संभावित समीकरणों का रूप होता है. ,

कलन विधि इसे फॉर्म के समीकरणों के समतुल्य समुच्चय में बदलने के लिए नियम प्रयुक्त करता है.

{ x₁ ≐ u₁, ..., x_m ≐ u_m }

जहाँ x₁, ..., x_m भिन्न-भिन्न चर हैं औरu₁, ..., u_m ऐसे पद हैं जिनमें x में से कोई भी नहीं है_i.

इस फॉर्म के एक समुच्चय को प्रतिस्थापन के रूप में पढ़ा जा सकता है।

यदि कोई हल नहीं है, तो कलन विधि ⊥ के साथ समाप्त हो जाता है; अन्य लेखक Ω , {} के रूप में उपयोग करते हैं या उस स्थिति में विफल हो जाते हैं।

समस्या G में चर x की सभी घटनाओं को पद t से प्रतिस्थापित करने की क्रिया को G {x ↦ t} दर्शाया गया है।

सरलता के लिए, स्थिर प्रतीकों को शून्य लॉजिक वाले फलन प्रतीकों के रूप में माना जाता है।

$G\cup \{t\doteq t\}$	$\Rightarrow$	$G$		delete
$G\cup \{f(s_{0},...,s_{k})\doteq f(t_{0},...,t_{k})\}$	$\Rightarrow$	$G\cup \{s_{0}\doteq t_{0},...,s_{k}\doteq t_{k}\}$		decompose
$G\cup \{f(s_{0},\ldots ,s_{k})\doteq g(t_{0},...,t_{m})\}$	$\Rightarrow$	$\bot$	if $f\neq g$ or $k\neq m$	conflict
$G\cup \{f(s_{0},...,s_{k})\doteq x\}$	$\Rightarrow$	$G\cup \{x\doteq f(s_{0},...,s_{k})\}$		swap
$G\cup \{x\doteq t\}$	$\Rightarrow$	$G\{x\mapsto t\}\cup \{x\doteq t\}$	if $x\not \in {\text{vars}}(t)$ and $x\in {\text{vars}}(G)$	eliminate^{[note 7]}
$G\cup \{x\doteq f(s_{0},...,s_{k})\}$	$\Rightarrow$	$\bot$	if $x\in {\text{vars}}(f(s_{0},...,s_{k}))$	check

ओक्कुर चेक

एक चर x को एक ऐसे पद के साथ एकीकृत करने का प्रयास जिसमें x एक सख्त उपपद x ≐ f(..., x, ...) के रूप में हो, x के हल के रूप में एक अनंत पद की ओर ले जाता है, क्योंकि x स्वयं के एक उपपद के रूप में घटित होता है

जैसा कि ऊपर परिभाषित किया गया है (परिमित) प्रथम-क्रम शब्दों के समुच्चय में समीकरण x ≐ f(..., x, ...) का कोई हल नहीं है; इसलिए उन्मूलन नियम मात्र तभी प्रयुक्त किया जा सकता है यदि x ∉ वार्स(t)।

चूँकि वह अतिरिक्त जाँच जिसे 'एक्सेस चेक' कहा जाता है, कलन विधि को धीमा कर देती है, इसलिए इसे छोड़ दिया जाता है, उदाहरण के लिए अधिकांश प्रोलॉग प्रणाली में होता है।

सैद्धांतिक दृष्टिकोण से, चेक को छोड़ना अनंत पेड़ों पर समीकरणों को हल करने के समतुल्य है, नीचे अनंत पदों का # एकीकरण के रूप में देख़ते है।

समाप्ति का प्रमाण

कलन विधि की समाप्ति के प्रमाण के लिए ट्रिपल पर विचार करें $\langle n_{var},n_{lhs},n_{eqn}\rangle$

जहाँ $n var$ समीकरण समुच्चय में एक से अधिक बार आने वाले चरों की संख्या है, $n lhs$ फलन प्रतीकों और स्थिरांकों की संख्या होती है'

संभावित समीकरणों के बाईं ओर और $n eqn$ समीकरणों की संख्या के रूप में है.

जब नियम उन्मूलन प्रयुक्त किया जाता है, $n var$ घट जाती है, क्योंकि G से x हटा दिया जाता है और मात्र { x ≐ t } में रखा जाता है।

कोई अन्य नियम प्रयुक्त करने से कभी वृद्धि नहीं हो सकती $n var$ दोबारा होता है ।

जब नियम विघटित, संघर्ष, या अदला-बदली प्रयुक्त के रूप में किया जाता है, $n lhs$ कम हो जाता है, क्योंकि कम से कम बायीं ओर का सबसे बाहरी f गायब हो जाता है।

बाकी किसी भी नियम को प्रयुक्त करने से डिलीट या चेक नहीं बढ़ सकेगा $n lhs$ , लेकिन घट जाती है $n eqn$ .

इसलिए किसी भी नियम को प्रयुक्त करने से तीन गुना कम हो जाता है $\langle n_{var},n_{lhs},n_{eqn}\rangle$ शब्दकोषीय क्रम के संबंध में जो मात्र सीमित संख्या में ही संभव है।

कॉनर मैकब्राइड देखते हैं^[20] एपिग्राम (प्रोग्रामिंग लैंग्वेज) जैसी आश्रित रूप से टाइप की गई लैंग्वेज में एकीकरण जिस संरचना का उपयोग करता है, उसे व्यक्त करके रॉबिन्सन के एकीकरण कलन विधि को चर की संख्या पर पुनरावर्ती बनाया जा सकता है, जिस स्थिति में एक भिन्न समाप्ति प्रमाण अनावश्यक हो जाता है।

प्रथम-क्रम शब्दों के वाक्यात्मकएकीकरण के उदाहरण

प्रोलॉग सिंटैक्टिकल कन्वेंशन में अपर केस अक्षर से प्रारंभ होने वाला प्रतीक एक परिवर्तनीय नाम है; एक प्रतीक जो छोटे अक्षर से प्रारंभ होता है. वह एक फलन प्रतीक है, अल्पविराम का उपयोग तार्किक और ऑपरेटर के रूप में किया जाता है।

गणितीय संकेतन के लिए, x,y,z को चर के रूप में, f,g को फलन प्रतीकों के रूप में, और a,b को स्थिरांक के रूप में उपयोग किया जाता है।

प्रकल संकेतन	गणितीय संकेतन	एकताकारी प्रतिस्थापन	निरूपण
`a = a`	{ a = a }	{}	सक्सीड (टॉटोलॉजी)
`a = b`	{ a = b }	⊥	a और b मेल नहीं खाते
`X = X`	{ x = x }	{}	सक्सीड (टॉटोलॉजी)
`a = X`	{ a = x }	{ x ↦ a }	x स्थिरांक के साथ एकीकृत है a
`X = Y`	{ x = y }	{ x ↦ y }	x और y अलियास हैं
`f(a,X) = f(a,b)`	{ f(a,x) = f(a,b) }	{ x ↦ b }	फलन और स्थिरांक प्रतीक मेल खाते हैं, x स्थिरांक b के साथ एकीकृत है
`f(a) = g(a)`	{ f(a) = g(a) }	⊥	`f`और`g`मेल नहीं खाते
`f(X) = f(Y)`	{ f(x) = f(y) }	{ x ↦ y }	x और y अलियास हैं
`f(X) = g(Y)`	{ f(x) = g(y) }	⊥	`f`और`g`मेल नहीं खाते
`f(X) = f(Y,Z)`	{ f(x) = f(y,z) }	⊥	फाल्स `f` फलन प्रतीकों में भिन्न -भिन्न योग्यताएं होती हैं
`f(g(X)) = f(Y)`	{ f(g(x)) = f(y) }	{ y ↦ g(x) }	y को पद के साथ एकीकृत करता है $g(x)$
`f(g(X),X) = f(Y,a)`	{ f(g(x),x) = f(y,a) }	{ x ↦ a, y ↦ g(a) }	x को स्थिरांक a के साथ और y को पद के साथ एकीकृत करता है $g(a)$
`X = f(X)`	{ x = f(x) }	should be ⊥	प्रथम-क्रम लॉजिक और कई आधुनिक प्रोलॉग बोलियों में रिटर्न ⊥ ओक्कुर चेक द्वारा प्रयुक्त होता है। पारंपरिक प्रोलॉग और प्रोलॉग II में`x`को अनंत पद के साथ एकीकृत करने में सफलता मिलती है`x=f(f(f(f(...))))`.
`X = Y, Y = a`	{ x = y, y = a }	{ x ↦ a, y ↦ a }	x और y दोनों स्थिरांक a के साथ एकीकृत हैं
`a = Y, X = Y`	{ a = y, x = y }	{ x ↦ a, y ↦ a }	जैसा कि ऊपर बताया गया है (समुच्चय में समीकरणों का क्रम मायने नहीं रखता हैं)
`X = a, b = X`	{ x = a, b = x }	⊥	फाल्स a और b मेल नहीं खाते हैं, इसलिए X को दोनों के साथ एकीकृत नहीं किया जा सकता है

अपने कम से कम सामान्य उदाहरण के लिए तेजी से बड़े पेड़ वाले दो शब्द। इसका निर्देशित चक्रीय आलेख प्रतिनिधित्व (सबसे दाहिना, नारंगी भाग) अभी भी रैखिक बनावट का है।

टर्म (लॉजिक )#शब्दों के साथ संचालन की वाक्यात्मक प्रथम क्रम एकीकरण समस्या का सबसे सामान्य एकीकरणकर्ता $n$ के रूप में बनावट हो सकता है $2 n$ . उदाहरण के लिए समस्या $(((a*z)*y)*x)*w\doteq w*(x*(y*(z*a)))$ में सबसे सामान्य एकीकरणकर्ता है' $\{z\mapsto a,y\mapsto a*a,x\mapsto (a*a)*(a*a),w\mapsto ((a*a)*(a*a))*((a*a)*(a*a))\}$ , सीf. चित्र। इस प्रकार के विस्फोट के कारण होने वाली घातीय समय जटिलता से बचने के लिए उन्नत एकीकरण कलन विधि पेड़ों के अतिरिक्त निर्देशित एसाइक्लिक आलेख़ (डैग) पर काम करते हैं।^[21]

अनुप्रयोग: लॉजिक प्रोग्रामिंग में एकीकरण

एकीकरण की अवधारणा लॉजिक प्रोग्रामिंग के पीछे मुख्य विचारों में से एक है, जिसे प्रोलॉग लैंग्वेज के माध्यम से जाना जाता है। यह चर की सामग्री को बांधने के तंत्र का प्रतिनिधित्व करता है और इसे एक प्रकार के एक बार के असाइनमेंट के रूप में देखा जा सकता है। प्रोलॉग में इस ऑपरेशन को समानता प्रतीक द्वारा दर्शाया जाता है = लेकिन चर को इंस्टेंटिएट करते समय भी किया जाता है (नीचे देखें)। समानता चिन्ह के प्रयोग से इसका प्रयोग अन्य लैंग्वेज में भी किया जाता है =अपितु कई ऑपरेशनों के संयोजन में भी सम्मिलित होता है +, -, *, /. प्रकार अनुमान कलन विधि सामान्यतः एकीकरण पर आधारित होते हैं।

प्रोलॉग में:

एक चर (प्रोग्रामिंग) जो अनइंस्टेंटिफाइड है—अर्थात् इस पर कोई पिछला एकीकरण नहीं किया गया था - इसे एक परमाणु, एक शब्द या किसी अन्य असंतुलित चर के साथ एकीकृत किया जा सकता है, इस प्रकार प्रभावी रूप से इसका अलियास बन जाता है। कई आधुनिक प्रोलॉग बोलियों और प्रथम-क्रम लॉजिक में एक चर को उस शब्द के साथ एकीकृत नहीं किया जा सकता है जिसमें वह सम्मिलित है; यह तथाकथित घटित जाँच है।
दो परमाणु तभी एकीकृत हो सकते हैं जब वे समान हों जाते है।
इसी प्रकार, एक पद को दूसरे पद के साथ एकीकृत किया जा सकता है यदि पदों के शीर्ष फलन प्रतीक और गुणधर्म समान हैं और यदि मापदंडों को एक साथ एकीकृत किया जा सकता है। ध्यान दें कि यह एक पुनरावर्ती व्यवहार है।

अनुप्रयोग: प्रकार अनुमान

कार्यात्मक लैंग्वेज हास्केल (प्रोग्रामिंग लैंग्वेज) और एमएल (प्रोग्रामिंग लैंग्वेज) सहित हिंडले-मिलनर प्रकार प्रणाली पर आधारित प्रकार प्रणालियों वाली लैंग्वेज के लिए प्रकार अनुमान के समय एकीकरण का उपयोग किया जाता है। एक ओर प्रोग्रामर को प्रत्येक फलन के लिए प्रकार की जानकारी प्रदान करने की आवश्यकता नहीं होती है, दूसरी ओर इसका उपयोग टाइपिंग त्रुटियों का पता लगाने के लिए किया जाता है। हास्केल अभिव्यक्तियों ट्रू : ['x', 'y', 'z'] सही ढंग से टाइप नहीं किया गया है. सूची निर्माण फलन (:) प्रकार का है a -> [a] -> [a], और पहले लॉजिक के लिएट्रूबहुरूपी प्रकार चर a के साथ एकाकार होना होगा ट्रूका प्रकार बूल. दूसरा लॉजिक , ['x', 'y', 'z'], प्रकार का है [चार], लेकिन a दोनों नहीं हो सकते बूल औरचार एक ही समय पर होते है.

प्रोलॉग के प्रकार अनुमान के लिए एक कलन विधि दिया जा सकता है:

कोई भी प्रकार का चर किसी भी प्रकार की अभिव्यक्तियों के साथ एकीकृत होता है और उस अभिव्यक्तियों के लिए त्वरित होता है। एक विशिष्ट सिद्धांत इस नियम को घटित जाँच के साथ प्रतिबंधित कर सकता है।
दो प्रकार के स्थिरांक तभी एकीकृत होते हैं जब वे एक ही प्रकार के हों जाते है।
दो प्रकार के निर्माण मात्र तभी एकीकृत होते हैं जब वे एक ही प्रकार के कंस्ट्रक्टर के अनुप्रयोग होते हैं और उनके सभी घटक प्रकार पुनरावर्ती रूप से एकीकृत होते हैं।

इसकी घोषणात्मक प्रकृति के कारण एकीकरण के अनुक्रम में क्रम (सामान्यतः) महत्वहीन है।

ध्यान दें कि प्रथम-क्रम लॉजिक की शब्दावली में, एक परमाणु एक मूल प्रस्ताव है और प्रोलॉग शब्द के समान एकीकृत है।

अनुप्रयोग: फ़ीचर संरचना एकीकरण

अभिकलनात्मक लैंग्वेज विज्ञान के विभिन्न अनुसंधान क्षेत्रों में एकीकरण के रूप में उपयोग किया गया है।^[22]^[23]

क्रमानुसार एकीकरण

क्रमबद्ध लॉजिक प्रत्येक पद के लिए एक सॉर्ट या प्रकार निर्दिष्ट करने और एक सॉर्ट s1 घोषित करने की अनुमति देता है, दूसरे प्रकार का एक उपवर्ग s₂, घोषित करने की अनुमति देता है, जिसे आमतौर पर s1 ⊆ s2 के रूप में लिखा जाता है। उदाहरण के लिए जैविक प्राणियों के बारे में लॉजिक करते समय एक प्रकार के कुत्ते को एक प्रकार के जानवर का उपवर्ग के रूप में घोषित करना उपयोगी होता है। जहां भी किसी प्रकार के शब्द की आवश्यकता होती है, उसके समष्टि पर किसी भी प्रकार के शब्द की आपूर्ति की जा सकती है।

उदाहरण के लिए एक फलन घोषणा मां: जानवर → जानवर, और एक निरंतर घोषणा लस्सी: कुत्ता मानते हुए, मां (लस्सी) शब्द पूरी प्रकार से मान्य है और इसमें जानवर की तरह है। यह जानकारी प्रदान करने के लिए कि कुत्ते की माँ बदले में एक कुत्ता है, एक और घोषणा माँ: कुत्ता → कुत्ता जारी की जा सकती है; इसे फलन ओवर लोडिंग कहा जाता है, प्रोग्रामिंग लैंग्वेज में ओवरलोडिंग के समान हो जाता है.

क्रिस्टोफ़ वाल्थर ने क्रम-क्रमबद्ध लॉजिक में शब्दों के लिए एक एकीकरण कलन विधि दिया जाता है, जिसके लिए किन्हीं दो घोषित प्रकारों की आवश्यकता होती हैs₁, s₂ उनका प्रतिच्छेदन s₁ ∩ s₂ घोषित किया जाना भी है : यदि x₁ और x₂ सॉर्ट का एक चर हैs₁,और s₂, क्रमशः, समीकरण x₁ ≐ x₂ हल के रूप में है {x₁ = x, x₂ = x }, जहां x: s₁ ∩ s₂.

^[24]इस कलन विधि को क्लॉज-आधारित स्वचालित प्रमेय कहावत में सम्मिलित करने के पश्चात, वह एक बेंचमार्क समस्या को क्रम-क्रमबद्ध लॉजिक में अनुवाद करके हल कर सकता है, जिससे इसे परिमाण के क्रम में उबाला जा सकता है, क्योंकि कई यूनरी विधेय प्रकार में बदल जाते हैं।

पैरामीट्रिक बहुरूपता की अनुमति देने के लिए स्मोल्का ने क्रम-क्रमबद्ध लॉजिक को सामान्यीकृत किया जाता है।

^[25]उनके ढांचे में उप-घोषणाएँ सम्मिश्र प्रकार की अभिव्यक्तियों के लिए प्रचारित की जाती हैं।

एक प्रोग्रामिंग उदाहरण के रूप में एक पैरामीट्रिक सॉर्ट सूची (X) घोषित की जा सकती है (टेम्प्लेट (C++)# फलन टेम्पलेट्स |C++ टेम्प्लेट में X एक प्रकार का पैरामीटर है), और एक सबसॉर्ट घोषणा से int ⊆ संबंध सूची फ़्लोट करें (int ) ⊆ सूची (फ्लोट) का स्वचालित रूप से अनुमान लगाया जाता है, जिसका अर्थ है कि पूर्णांकों की प्रत्येक सूची भी फ्लोट्स की एक सूची है।

श्मिट-शाउß ने शब्द घोषणाओं की अनुमति देने के लिए क्रम-क्रमबद्ध लॉजिक को सामान्यीकृत किया। ^[26] उदाहरण के तौर पर, उपवर्ग घोषणाओं को सम ⊆ int और विषम ⊆ int मानते हुए, एक शब्द घोषणा जैसे ∀ i : int। (i + i): पूर्णांक जोड़ की एक गुणधर्म घोषित करने की भी अनुमति देता है जिसे सामान्य ओवरलोडिंग द्वारा व्यक्त नहीं किया जा सकता है।

अनंत पदों का एकीकरण

अनंत पेड़ों पर पृष्ठभूमि:

बी कौरसेल (1983). "अनंत ट्री के मौलिक गुण". सैद्धांतिक संगणना विज्ञान. 25 (2): 95–169. doi:10.1016/0304-3975(83)90059-2.
माइकल जे. महर (जुलाई 1988)"परिमित, तर्कसंगत और अनंत पेड़ों के बीजगणित के पूर्ण स्वयंसिद्ध!"प्रोक. आईईईई तीसरा वार्षिक संगोष्ठी पर कंप्यूटर विज्ञान में तर्क, एडिनबर्ग.पृ. 348-357
Joxan Jaffar; Peter J. Stuckey (1986). "अनंत वृक्ष तर्क प्रोग्रामिंग के शब्दार्थ". Theoretical Computer Science. 46: 141–158. doi:10.1016/0304-3975(86)90027-7.

एकीकरण कलन विधि , प्रोलॉग II:

ए कोलमेरौएर (1982). के.एल. क्लार्क; एस.-ए. टार्नलुंड (eds.). प्रोलॉग और अनंत पेड़. अकादमिक प्रेस.
एलेन कोलम्योर (1984)"परिमित और अनंत पेड़ों पर समीकरण और असमानताएं"आईसीयू (एडी) में प्रक्रिया समझौता। पांचवीं पीढ़ी कंप्यूटर सिस्टम पर पृ. 85-99 अनुप्रयोग।

फ्रांसिस जियानेसिनी; जैक्स कोहेन (1984). "प्रोलॉग के अनंत पेड़ों का उपयोग करके पार्सर जेनरेशन और व्याकरण हेरफेर". जर्नल ऑफ़ लॉजिक प्रोग्रामिंग. 1 (3): 253–265. doi:10.1016/0743-1066(84)90013-X.

ई-एकीकरण

ई- एकीकरण समीकरण के दिए गए समुच्चय का हल खोजने की समस्या है.

कुछ समीकरणात्मक पृष्ठभूमि ज्ञान E को ध्यान में रखते हुए।

उत्तरार्द्ध को सार्वभौमिक समानता के एक समुच्चय के रूप में दिया गया है।

कुछ विशेष समुच्चय E के लिए समीकरण हल करने वाले कलन विधि (उर्फ ई- एकीकरण एल्गोरिदम) तैयार किए गए हैं;

दूसरों के लिए यह सिद्ध हो चुका है कि ऐसा कोई कलन विधि उपलब्ध नहीं हो सकता है।

उदाहरण के लिए, यदि $a$ और $b$ विशिष्ट स्थिरांक हैं,

समीकरण $x*a\doteq y*b$ का कोई हल नहीं है.

विशुद्ध वाक्यात्मकएकीकरण में संबंध हो जाता है

जहां संचालक के बारे में कुछ भी पता नहीं चल पाया है $*$ .

चूंकि यदि $*$ क्रमविनिमेय माना जाता है,

फिर प्रतिस्थापन ${x \mapsto b, y \mapsto a}$ उपरोक्त समीकरण को हल करता है,

जब से,

	$x*a$	${x \mapsto b, y \mapsto a}$
=	$b*a$		प्रतिस्थापन अनुप्रयोग द्वारा
=	$a*b$		की क्रमपरिवर्तनशीलता द्वारा $*$
=	$y*b$	${x \mapsto b, y \mapsto a}$	(विपरीत) प्रतिस्थापन अनुप्रयोग द्वारा

पृष्ठभूमि ज्ञान E की क्रम परिवर्तनशीलता बता सकता है $*$ सार्वभौम समानता द्वारा $u*v=v*u$ सभी के लिए $u, v$ .

विशेष पृष्ठभूमि ज्ञान समुच्चय E

**Used naming conventions**
$\forall u, v, w :$	$u(vw)$	=	$(uv)w$	$A$	की संबद्धता $*$
$\forall u, v :$	$u*v$	=	$v*u$	$C$	की क्रमपरिवर्तनशीलता $*$
$\forall u, v, w :$	$u*(v+w)$	=	$uv+uw$	$D l$	का वाम वितरण ∗ ऊपर +
$\forall u, v, w :$	$(v+w)*u$	=	$vu+wu$	$D r$	का सही वितरण ∗ ऊपर +
$\forall u :$	$u*u$	=	$u$	$I$	नपुंसकताof $*$
$\forall u :$	$n*u$	=	$u$	$N l$	के संबंध में तटस्थ तत्व n छोड़ दिया $*$
$\forall u :$	$u*n$	=	$u$	$N r$	के संबंध में सही तटस्थ तत्व n ** $*$

ऐसा कहा जाता है कि एकीकरण एक सिद्धांत के लिए निर्णायक होता है, यदि इसके लिए एक एकीकरण कलन विधि तैयार किया गया है, जो किसी भी इनपुट समस्या के लिए समाप्त हो जाता है।

ऐसा कहा जाता है कि एकीकरण एक सिद्धांत के लिए अर्ध-निर्णायक है, यदि इसके लिए एक एकीकरण कलन विधि तैयार किया गया है, जो किसी भी हल करने योग्य इनपुट समस्या के लिए समाप्त हो जाता है, लेकिन एक अघुलनशील इनपुट समस्या के हल के लिए निरंतर के लिए खोज जारी रख सकता है।

निम्नलिखित सिद्धांतों के लिए ' एकीकरण निर्णायक है':

' $A$ ^[27]
$A$ , $C$ ^[28]
$A$ , $C$ , $I$ ^[29]
$A$ , $C$ , $N l$ ^{[note 8]}^[29]* $A$ , $I$ ^[30]
$A$ , $N l$ $,$ $N r$ (मोनॉइड)^[31]
$C$ ^[32]
बूलियन रिंग^[33]^[34]
एबेलियन समूह, यदि हस्ताक्षर को यादृच्छिक ढंग से अतिरिक्त प्रतीकों द्वारा विस्तारित किया गया हो (लेकिन स्वयंसिद्ध नहीं)^[35]
क्रिपके शब्दार्थ#पत्राचार और पूर्णता मोडल बीजगणित^[36]

निम्नलिखित सिद्धांतों के लिए एकीकरण अर्ध-निर्णायक है:

$A$ , $D l$ $,$ $D r$ ^[37]
$A$ , $C$ , $D l$ ^{[note 8]}^[38]
क्रमविनिमेय वलय^[35]

एकतरफा पैरामोड्यूलेशन

यदि E के लिए एक अभिसरण शब्द पुनर्लेखन प्रणाली आर उपलब्ध है,

'एकतरफा पैरामोड्यूलेशन' एल्गोरिदम^[39]

दिए गए समीकरणों के सभी समाधानों के रूप में गिनने के लिए उपयोग किया जा सकता है।

एकतरफ़ा पैरामॉड्यूलेशन नियम
G ∪ { f(s₁,...,s_n) ≐ f(t₁,...,t_n) }	; S	⇒	G ∪ { s₁ ≐ t₁, ..., s_n ≐ t_n }	; S		decompose
G ∪ { x ≐ t }	; S	⇒	G { x ↦ t }	; S{x↦t} ∪ {x↦t}	if the variable x doesn't occur in t	eliminate
G ∪ { f(s₁,...,s_n) ≐ t }	; S	⇒	G ∪ { s₁ ≐ u₁, ..., s_n ≐ u_n, r ≐ t }	; S	if f(u₁,...,u_n) → r is a rule from R	mutate
G ∪ { f(s₁,...,s_n) ≐ y }	; S	⇒	G ∪ { s₁ ≐ y₁, ..., s_n ≐ y_n, y ≐ f(y₁,...,y_n) }	; S	if y₁,...,y_n are new variables	imitate

G से प्रारंभ करके हल की जाने वाली एकीकरण समस्या और S पहचान प्रतिस्थापन है, नियमों को गैर-नियतात्मक रूप से प्रयुक्त किया जाता है, जब तक कि खाली समुच्चय वास्तविक G के रूप में प्रकट नहीं होता है, इस स्थिति में वास्तविक S एक एकीकृत प्रतिस्थापन है। आदेश के आधार पर पैरामॉड्यूलेशन नियम प्रयुक्त होते हैं, G से वास्तविक समीकरण की पसंद पर और R की पसंद पर'के नियमों में परिवर्तन, विभिन्न संगणना पथ संभव हैं। मात्र कुछ ही हल की ओर ले जाते हैं, जबकि अन्य G ≠ {} पर समाप्त होते हैं, जहां कोई और नियम प्रयुक्त नहीं होता है. (जैसे G = { f(...) ≐ g(...) })।

Example term rewrite system R
1	app(nil,z)	→ z
2	app(x.y,z)	→ x.app(y,z)

उदाहरण के लिए एक शब्द रीराइट प्रणाली R का उपयोग विपक्ष और शून्य से निर्मित सूचियों के परिशिष्ट ऑपरेटर को परिभाषित करने के लिए किया जाता है; जहां संक्षिप्तता के लिए cons(x,y) को इन्फ़िक्स नोटेशन में x.y के रूप में लिखा जाता है; जैसे ऐप(a.b.nil,c.d.nil) → a.app(b.nil,c.d.nil) → a.b.app(nil,c.d.nil) → a.b.c.d.nil सूचियों a.b.nil और c.d.nil के संयोजन को प्रदर्शित करता है, पुनर्लेखन नियम 2 का उपयोग करते हुए, 2, और 1. R के अनुरूप समीकरण सिद्धांत E, R का सर्वांगसम समापन है, दोनों को शर्तों पर द्विआधारी संबंध के रूप में देखा जाता है।

उदाहरण के लिए, ऐप(a.b.nil,c.d.nil) ≡ a.b.c.d.nil ≡ ऐप(a.b.c.d.nil,nil)। पैरामोड्यूलेशन कलन विधि उदाहरण R के साथ दिए जाने पर उस E के संबंध में समीकरणों के हल की गणना करता है।

एकीकरण समस्या {app(x,app(y,x)) ≐ a.a.nil } के लिए एक सफल उदाहरण गणना पथ नीचे दिखाया गया है। परिवर्तनीय नाम टकराव से बचने के लिए, नियम परिवर्तन द्वारा उनके उपयोग से पहले हर बार पुनर्लेखन नियमों का लगातार नाम बदला जाता है; v₂, v₃, ... इस उद्देश्य के लिए कंप्यूटर-जनित परिवर्तनीय नाम हैं। प्रत्येक पंक्ति में, G से चुना गया समीकरण लाल रंग में हाइलाइट किया गया है। हर बार जब उत्परिवर्तित नियम प्रयुक्त किया जाता है, तो चुने गए पुनर्लेखन नियम (1 या 2) को कोष्ठक में दर्शाया जाता है। अंतिम पंक्ति से एकीकृत प्रतिस्थापन S = {y ↦ nil, x ↦ a.nil } प्राप्त किया जा सकता है। वास्तव में,

ऐप(x,ऐप(y,x)) {y↦nil, x↦ a.nil } = ऐप(a.nil,app(nil,a.nil)) ≡ ऐप(a.nil,a.nil) ≡ a.app(nil,a.nil) ≡ a.a.nil दी गई समस्या का हल करता है।

दूसरा सफल संगणना पथ, जिसे mutate(1), mutate(2), mutate(2), mutate(1) चुनकर प्राप्त किया जा सकता है, प्रतिस्थापन की ओर ले जाता है S = { y ↦ a.a.nil, x ↦ nil }; यह यहां नहीं दिखाया गया है. कोई अन्य मार्ग सफलता की ओर नहीं ले जाता।

उदाहरण एकीकरण अभिकलन
प्रयुक्त नियम		G	S
		{ app(x,app(y,x)) ≐ a.a.nil }	{}
म्यूटेट(2)	⇒	{ x ≐ v₂.v₃, app(y,x) ≐ v₄, v₂.app(v₃,v₄) ≐ a.a.nil }	{}
डीकोम्पोस	⇒	{ x ≐ v₂.v₃, app(y,x) ≐ v₄, v₂ ≐ a, app(v₃,v₄) ≐ a.nil }	{}
एलिमिनेट	⇒	{ app(y,v₂.v₃) ≐ v₄, v₂ ≐ a, app(v₃,v₄) ≐ a.nil }	{ x ↦ v₂.v₃ }
एलिमिनेट	⇒	{ app(y,a.v₃) ≐ v₄, app(v₃,v₄) ≐ a.nil }	{ x ↦ a.v₃ }
mutate(1)	⇒	{ y ≐ nil, a.v₃ ≐ v₅, v₅ ≐ v₄, app(v₃,v₄) ≐ a.nil }	{ x ↦ a.v₃ }
एलिमिनेट	⇒	{ y ≐ nil, a.v₃ ≐ v₄, app(v₃,v₄) ≐ a.nil }	{ x ↦ a.v₃ }
एलिमिनेट	⇒	{ a.v₃ ≐ v₄, app(v₃,v₄) ≐ a.nil }	{ y ↦ nil, x ↦ a.v₃ }
म्यूटेट(1)	⇒	{ a.v₃ ≐ v₄, v₃ ≐ nil, v₄ ≐ v₆, v₆ ≐ a.nil }	{ y ↦ nil, x ↦ a.v₃ }
एलिमिनेट	⇒	{ a.v₃ ≐ v₄, v₃ ≐ nil, v₄ ≐ a.nil }	{ y ↦ nil, x ↦ a.v₃ }
एलिमिनेट	⇒	{ a.nil ≐ v₄, v₄ ≐ a.nil }	{ y ↦ nil, x ↦ a.nil }
एलिमिनेट	⇒	{ a.nil ≐ a.nil }	{ y ↦ nil, x ↦ a.nil }
डीकोम्पोस	⇒	{ a ≐ a, nil ≐ nil }	{ y ↦ nil, x ↦ a.nil }
डीकोम्पोस	⇒	{ nil ≐ nil }	{ y ↦ nil, x ↦ a.nil }
डीकोम्पोस	⇒	{}	{ y ↦ nil, x ↦ a.nil }

संकुचन

पुनर्लेखन नियम का उपयोग करते हुए एकीकृत प्रतिस्थापन σ (निचली पंक्ति) के साथ, पद s में स्थिति p पर चरण s ↝ t को संकीर्ण करने का त्रिभुज आरेख

l \to r

(सबसे ऊपर की कतार)

यदि R, E के लिए एक अभिसारी पद पुनर्लेखन प्रणाली है,

पिछले अनुभाग के लिए एक दृष्टिकोण विकल्प में 'संकीर्ण चरणों' का क्रमिक अनुप्रयोग सम्मिलित है;

यह अंततः किसी दिए गए समीकरण के सभी समाधानों की गणना करेगा।

एक संकीर्ण चरण (cf. चित्र) के रूप में सम्मिलित है

वर्तमान पद का एक गैर-परिवर्तनीय उपपद चुनना है,
आर से एक नियम के बाईं ओर इसे वाक्यात्मकरूप से एकीकृत करना, और
तात्कालिक नियम के दाहिने हाथ को तात्कालिक शब्द में बदलना होता है।

फॉर्मल रूप से, यदि $l \to r$ आर से पुनर्लेखन नियम की एक पुनर्नामित प्रति है, जिसमें शब्द एस और उपपद के साथ कोई चर समान नहीं है $s | p$ एक चर नहीं है और इसके साथ एकीकृत किया जा सकता है $l$ प्रथम-क्रम शब्दों के # वाक्यात्मकएकीकरण के माध्यम से $σ$ , तब $s$ को इस शब्द तक सीमित किया जा सकता है $t = sσ [rσ] p$ , अर्थात पद के लिए $sσ$ , पी पर सबटर्म के साथ टर्म (लॉजिक)#ऑपरेशन्स विद टर्म्स बाय $rσ$ . वह स्थिति जिसमें s को t तक सीमित किया जा सकता है, सामान्यतः s ↝ t के रूप में निरूपित की जाती है।

सहज रूप से, संकीर्ण चरणों का एक क्रम टी₁ ↝ टी₂ ↝ ... ↝ टी_n इसे पुनः लिखने के चरणों के अनुक्रम के रूप में सोचा जा सकता है₁ → टी₂ → ... → टी_n, लेकिन प्रारंभिक पद t के साथ₁ प्रत्येक प्रयुक्त नियम को प्रयुक्त करने के लिए आवश्यकतानुसार इसे और अधिक त्वरित किया जा रहा है।

एकतरफा पैरामॉड्यूलेशन उदाहरण पैरामॉड्यूलेशन गणना निम्नलिखित संकीर्ण अनुक्रम से मेल खाती है (↓ यहां तात्कालिकता का संकेत है):

app(

x

,app(y,

x

))

↓

x ↦ v₂.v₃

app(

v₂.v₃

,app(y,

v₂.v₃

))

→

v₂.app(v₃,app(

y

,v₂.v₃))

↓

y ↦ nil

v₂.app(v₃,app(

nil

,v₂.v₃))

→

v₂.app(

v₃

,v₂.

v₃

)

↓

v₃ ↦ nil

v₂.app(

nil

,v₂.

nil

)

→

v₂.v₂.nil

अंतिम पद, वी₂।में₂.nil को मूल दाहिनी ओर के शब्द a.a.nil के साथ वाक्यात्मकरूप से एकीकृत किया जा सकता है।

सिकुड़ती लेम्मा^[40] यह सुनिश्चित करता है कि जब भी किसी शब्द के उदाहरण को एक अभिसरण शब्द पुनर्लेखन प्रणाली द्वारा किसी शब्द t में फिर से लिखा जा सकता है, तो s और t को संकुचित किया जा सकता है और एक शब्द में फिर से लिखा जा सकता है $s'$ और $t'$ , क्रमशः, ऐसे कि $t'$ का एक उदाहरण है $s'$ .

फॉर्मल रूप से: जब भी $sσ \to * t$ कुछ प्रतिस्थापन के लिए σ रखता है, तो वहां शर्तें उपलब्ध हैं $s', t'$ ऐसा है कि $s ↝ * s'$ और $t \to * t'$ और $s' τ = t'$ कुछ प्रतिस्थापन के लिए τ.

उच्च-क्रम एकीकरण

गोल्डफ़ार्ब में^[41]हिल्बर्ट की 10वीं समस्या को दूसरे क्रम की एकीकरणीयता, समीकरण में घटाना

X_{1}*X_{2}=X_{3}

फलन चर के साथ चित्रित एकीकरण समस्या से मेल खाता है

F_{i}

तदनुसार

X_{i}

और

G

ताजा चर.

कई अनुप्रयोगों के लिए प्रथम-क्रम शब्दों के अतिरिक्त टाइप किए गए लैम्ब्डा-शब्दों के एकीकरण पर विचार करने की आवश्यकता होती है। इस प्रकार के एकीकरण को अधिकांशतः उच्च-क्रम एकीकरण कहा जाता है। उच्च-क्रम एकीकरण अनिर्णीत समस्या है,^[41]^[42]^[43] और ऐसी एकीकरण समस्याओं में अधिकांश सामान्य एकीकरणकर्ता नहीं होते हैं। उदाहरण के लिए, एकीकरण समस्या { f(a,b,a) ≐ d(b,a,c) }, जहां एकमात्र चर f है, में है

हल {f ↦ λx.λy.λz. d(y,x,c) }, {f ↦ λx.λy.λz. d(y,z,c) }, {f ↦ λx.λy.λz. d(y,a,c) }, {f ↦ λx.λy.λz. डी(बी,x,सी) },

{f ↦ λx.λy.λz. d(b,z,c) } और {f ↦ λx.λy.λz. डी(बी,ए,सी) }. उच्च-क्रम एकीकरण की एक अच्छी प्रकार से अध्ययन की गई शाखा αβη रूपांतरणों द्वारा निर्धारित समानता को सरल रूप से टाइप किए गए लैम्ब्डा शब्दों मॉड्यूलो को एकीकृत करने की समस्या है। जेरार्ड ह्यूएट ने एक अर्ध-निर्णायक (पूर्व) एकीकरण कलन विधि दिया^[44] जो एकीकरणकर्ताओं के समष्टि की व्यवस्थित खोज की अनुमति देता है (मार्टेली-मोंटानारी के एकीकरण कलन विधि को सामान्यीकृत करना)^[9]उच्च-क्रम वाले चर वाले शब्दों के नियमों के साथ) जो व्यवहार में पर्याप्त रूप से अच्छी प्रकार से काम करता प्रतीत होता है। Huet^[45] और गाइल्स डोवेक^[46] इस विषय पर सर्वेक्षण करते हुए लेख लिखे हैं।

उच्च-क्रम एकीकरण के कई उपसमूह अच्छी प्रकार से व्यवहार किए जाते हैं, जिसमें वे निर्णय लेने योग्य होते हैं और हल करने योग्य समस्याओं के लिए सबसे सामान्य एकीकरणकर्ता होते हैं। ऐसा एक उपसमुच्चय पहले वर्णित प्रथम-क्रम पद है। डेल मिलर के कारण उच्च-क्रम पैटर्न एकीकरण,^[47] ऐसा ही एक और उपसमुच्चय है। उच्च-क्रम लॉजिक प्रोग्रामिंग लैंग्वेजएं λप्रोलॉग और ट्वेल्फ़ पूर्ण उच्च-क्रम एकीकरण से मात्र पैटर्न खंड को प्रयुक्त करने के लिए स्विच कर चुकी हैं; आश्चर्यजनक रूप से पैटर्न एकीकरण लगभग सभी कार्यक्रमों के लिए पर्याप्त है, यदि प्रत्येक गैर-पैटर्न एकीकरण समस्या को तब तक निलंबित कर दिया जाता है जब तक कि अगला प्रतिस्थापन एकीकरण को पैटर्न खंड में नहीं डाल देता। पैटर्न एकीकरण का एक सुपरसमुच्चय जिसे फलन -एज़-कंस्ट्रक्टर्स एकीकरण कहा जाता है, भी अच्छी प्रकार से व्यवहार किया जाता है।^[48] ज़िपरपोज़िशन प्रमेय कहावत में एक कलन विधि है जो इन अच्छे व्यवहार वाले उपसमुच्चय को पूर्ण उच्च-क्रम एकीकरण कलन विधि में एकीकृत करता है।^[6]

अभिकलनात्मक लैंग्वेज विज्ञान में अण्डाकार निर्माण के सबसे प्रभावशाली सिद्धांतों में से एक यह है कि दीर्घवृत्त को मुक्त चर द्वारा दर्शाया जाता है, जिनके मान तब उच्च-क्रम एकीकरण का उपयोग करके निर्धारित किए जाते हैं। उदाहरण के लिए जॉन का अर्थपूर्ण प्रतिनिधित्व मैरी को पसंद है और पीटर को भी पसंद है $like(j, m) \land R(p)$ और आर का मान (दीर्घवृत्त का अर्थपूर्ण प्रतिनिधित्व) समीकरण द्वारा निर्धारित किया जाता है $like(j, m) = R(j)$ . ऐसे समीकरणों को हल करने की प्रक्रिया को उच्च-क्रम एकीकरण कहा जाता है।^[49]

वेन स्नाइडर ने उच्च-क्रम एकीकरण और ई- एकीकरण दोनों का सामान्यीकरण दिया, अर्थात लैम्ब्डा-शब्द मॉड्यूलो को एक समीकरण सिद्धांत को एकीकृत करने के लिए एक एल्गोरिदम।^[50]

यह भी देखें

पुनर्लेखन
स्वीकार्य नियम
लैम्ब्डा कैलकुलस में स्पष्ट प्रतिस्थापन
गणितीय समीकरण हल करना
डिस- एकीकरण (कंप्यूटर विज्ञान)|डिस-यूनिफिकेशन: सिंबॉलिक अभिव्यक्तियों के बीच असमानताओं को हल करना
एंटी- एकीकरण (कंप्यूटर साइंस)|एंटी-यूनिफिकेशन: दो शब्दों के कम से कम सामान्य सामान्यीकरण (एलजीजी) की गणना करना, सबसे सामान्य उदाहरण (एमजीयू) की गणना करना
सब्समिशन जाली, एक जाली जिसमें मिलन के रूप में एकीकरण और जुड़ने के रूप में विरोधी एकीकरण होता है
ओन्टोलॉजी संरेखण (शब्दार्थ तुल्यता के साथ एकीकरण का उपयोग करें)

↑ E.g. a ⊕ (b ⊕ f(x)) ≡ a ⊕ (f(x) ⊕ b) ≡ (b ⊕ f(x)) ⊕ a ≡ (f(x) ⊕ b) ⊕ a
↑ since $(x\oplus y)\{x\mapsto z,y\mapsto z\}=z\oplus z\equiv z$
↑ since $z {z \mapsto x \oplus y} = x \oplus y$
↑ formally: each unifier τ satisfies $\forall x : xτ = (xσ) ρ$ for some substitution ρ
↑ Alg.1, p.261. Their rule (a) corresponds to rule swap here, (b) to delete, (c) to both decompose and conflict, and (d) to both eliminate and check.
↑ Independent discovery is stated in Martelli, Montanari (1982),^[9] sect.1, p.259. Paterson's and Wegman's journal paper^[16] is dated 1978; however, the journal publisher received it in Sep.1976.
↑ Although the rule keeps x ≐ t in G, it cannot loop forever since its precondition x∈vars(G) is invalidated by its first application. More generally, the algorithm is guaranteed to terminate always, see below.
↑ ^8.0 ^8.1 in the presence of equality $C$ , equalities $N l$ and $N r$ are equivalent, similar for $D l$ and $D r$

संदर्भ

↑ J. Herbrand: Recherches sur la théorie de la démonstration. Travaux de la société des Sciences et des Lettres de Varsovie, Class III, Sciences Mathématiques et Physiques, 33, 1930.
↑ Claus-Peter Wirth; Jörg Siekmann; Christoph Benzmüller; Serge Autexier (2009). एक तर्कशास्त्री के रूप में जैक्स हेरब्रांड पर व्याख्यान (SEKI Report). DFKI. arXiv:0902.4682. Here: p.56
↑ Jacques Herbrand (1930). Recherches sur la théorie de la demonstration (PDF) (Ph.D. thesis). A. Vol. 1252. Université de Paris. Here: p.96-97
↑ ^4.0 ^4.1 ^4.2 ^4.3 J.A. Robinson (Jan 1965). "संकल्प सिद्धांत पर आधारित एक मशीन-उन्मुख तर्क". Journal of the ACM. 12 (1): 23–41. doi:10.1145/321250.321253. S2CID 14389185.; Here: sect.5.8, p.32
↑ J.A. Robinson (1971). "Computational logic: The unification computation". Machine Intelligence. 6: 63–72.
↑ ^6.0 ^6.1 ^6.2 Vukmirović, Petar; Bentkamp, Alexander; Nummelin, Visa (14 December 2021). "कुशल पूर्ण उच्च-क्रम एकीकरण". Logical Methods in Computer Science. 17 (4): 6919. doi:10.46298/lmcs-17(4:18)2021.
↑ Apt, Krzysztof R. (1997). लॉजिक प्रोग्रामिंग से लेकर प्रोलॉग तक (1. publ ed.). London Munich: Prentice Hall. p. 24. ISBN 013230368X.
↑ Fages, François; Huet, Gérard (1986). "समीकरण सिद्धांतों में यूनिफायर और मैचर्स का पूरा सेट". Theoretical Computer Science. 43: 189–200. doi:10.1016/0304-3975(86)90175-1.
↑ ^9.0 ^9.1 ^9.2 Martelli, Alberto; Montanari, Ugo (Apr 1982). "एक कुशल एकीकरण एल्गोरिदम". ACM Trans. Program. Lang. Syst. 4 (2): 258–282. doi:10.1145/357162.357169. S2CID 10921306.
↑ Robinson (1965);^[4] nr.2.5, 2.14, p.25
↑ Robinson (1965);^[4] nr.5.6, p.32
↑ Robinson (1965);^[4] nr.5.8, p.32
↑ Lewis Denver Baxter (Feb 1976). एक व्यावहारिक रूप से रैखिक एकीकरण एल्गोरिदम (PDF) (Res. Report). Vol. CS-76-13. Univ. of Waterloo, Ontario.
↑ Gérard Huet (Sep 1976). Resolution d'Equations dans des Langages d'Ordre 1,2,...ω (These d'etat). Universite de Paris VII.
↑ ^15.0 ^15.1 Alberto Martelli & Ugo Montanari (Jul 1976). Unification in linear time and space: A structured presentation (Internal Note). Vol. IEI-B76-16. Consiglio Nazionale delle Ricerche, Pisa. Archived from the original on 2015-01-15.
↑ ^16.0 ^16.1 ^16.2 ^16.3 Michael Stewart Paterson and M.N. Wegman (Apr 1978). "रैखिक एकीकरण". J. Comput. Syst. Sci. 16 (2): 158–167. doi:10.1016/0022-0000(78)90043-0.
↑ J.A. Robinson (Jan 1976). "Fast unification". In Woodrow W. Bledsoe, Michael M. Richter (ed.). प्रोक. प्रमेय सिद्ध करने की कार्यशाला ओबेरवुल्फ़च. Oberwolfach Workshop Report. Vol. 1976/3.^{[permanent dead link]}
↑ M. Venturini-Zilli (Oct 1975). "प्रथम-क्रम अभिव्यक्तियों के लिए एकीकरण एल्गोरिथ्म की जटिलता". Calcolo. 12 (4): 361–372. doi:10.1007/BF02575754. S2CID 189789152.
↑ Paterson, M.S.; Wegman, M.N. (May 1976). Chandra, Ashok K.; Wotschke, Detlef; Friedman, Emily P.; Harrison, Michael A. (eds.). रैखिक एकीकरण. Proceedings of the eighth annual ACM Symposium on Theory of Computing (STOC). ACM. pp. 181–186. doi:10.1145/800113.803646.
↑ McBride, Conor (October 2003). "संरचनात्मक प्रत्यावर्तन द्वारा प्रथम-क्रम एकीकरण". Journal of Functional Programming. 13 (6): 1061–1076. CiteSeerX 10.1.1.25.1516. doi:10.1017/S0956796803004957. ISSN 0956-7968. S2CID 43523380. Retrieved 30 March 2012.
↑ e.g. Paterson, Wegman (1978),^[16] sect.2, p.159
↑ Jonathan Calder, Mike Reape, and Hank Zeevat,, An algorithm for generation in unification categorial grammar. In Proceedings of the 4th Conference of the European Chapter of the Association for Computational Linguistics, pages 233-240, Manchester, England (10–12 April), University of Manchester Institute of Science and Technology, 1989.
↑ Graeme Hirst and David St-Onge, [1] Lexical chains as representations of context for the detection and correction of malapropisms, 1998.
↑ Walther, Christoph (1985). "कई-क्रमबद्ध रिज़ॉल्यूशन द्वारा शुबर्ट के स्टीमरोलर का एक यांत्रिक समाधान" (PDF). Artif. Intell. 26 (2): 217–224. doi:10.1016/0004-3702(85)90029-3. Archived from the original (PDF) on 2011-07-08. Retrieved 2013-06-28.
↑ Smolka, Gert (Nov 1988). पॉलिमॉर्फिकली ऑर्डर-सॉर्टेड प्रकारों के साथ लॉजिक प्रोग्रामिंग (PDF). Int. Workshop Algebraic and Logic Programming. LNCS. Vol. 343. Springer. pp. 53–70. doi:10.1007/3-540-50667-5_58.
↑ Schmidt-Schauß, Manfred (Apr 1988). टर्म घोषणाओं के साथ ऑर्डर-सॉर्टेड लॉजिक के कम्प्यूटेशनल पहलू. Lecture Notes in Artificial Intelligence (LNAI). Vol. 395. Springer.
↑ Gordon D. Plotkin, Lattice Theoretic Properties of Subsumption, Memorandum MIP-R-77, Univ. Edinburgh, Jun 1970
↑ Mark E. Stickel, A Unification Algorithm for Associative-Commutative Functions, J. Assoc. Comput. Mach., vol.28, no.3, pp. 423–434, 1981
↑ ^29.0 ^29.1 F. Fages, Associative-Commutative Unification, J. Symbolic Comput., vol.3, no.3, pp. 257–275, 1987
↑ Franz Baader, Unification in Idempotent Semigroups is of Type Zero, J. Automat. Reasoning, vol.2, no.3, 1986
↑ J. Makanin, The Problem of Solvability of Equations in a Free Semi-Group, Akad. Nauk SSSR, vol.233, no.2, 1977
↑ F. Fages (1987). "साहचर्य-अनुकरणीय एकीकरण" (PDF). J. Symbolic Comput. 3 (3): 257–275. doi:10.1016/s0747-7171(87)80004-4.
↑ Martin, U., Nipkow, T. (1986). "Unification in Boolean Rings". In Jörg H. Siekmann (ed.). Proc. 8th CADE. LNCS. Vol. 230. Springer. pp. 506–513.{{cite book}}: CS1 maint: multiple names: authors list (link)
↑ A. Boudet; J.P. Jouannaud; M. Schmidt-Schauß (1989). "बूलियन रिंग्स और एबेलियन समूहों का एकीकरण". Journal of Symbolic Computation. 8 (5): 449–477. doi:10.1016/s0747-7171(89)80054-9.
↑ ^35.0 ^35.1 Baader and Snyder (2001), p. 486.
↑ F. Baader and S. Ghilardi, Unification in modal and description logics, Logic Journal of the IGPL 19 (2011), no. 6, pp. 705–730.
↑ P. Szabo, Unifikationstheorie erster Ordnung (First Order Unification Theory), Thesis, Univ. Karlsruhe, West Germany, 1982
↑ Jörg H. Siekmann, Universal Unification, Proc. 7th Int. Conf. on Automated Deduction, Springer LNCS vol.170, pp. 1–42, 1984
↑ N. Dershowitz and G. Sivakumar, Solving Goals in Equational Languages, Proc. 1st Int. Workshop on Conditional Term Rewriting Systems, Springer LNCS vol.308, pp. 45–55, 1988
↑ Fay (1979). "First-Order Unification in an Equational Theory". Proc. 4th Workshop on Automated Deduction. pp. 161–167.
↑ ^41.0 ^41.1 Warren D. Goldfarb (1981). "द्वितीय-क्रम एकीकरण समस्या की अनिर्णयता". TCS. 13 (2): 225–230. doi:10.1016/0304-3975(81)90040-2.
↑ Gérard P. Huet (1973). "तीसरे क्रम के तर्क में एकीकरण की अनिश्चितता". Information and Control. 22 (3): 257–267. doi:10.1016/S0019-9958(73)90301-X.
↑ Claudio Lucchesi: The Undecidability of the Unification Problem for Third Order Languages (Research Report CSRR 2059; Department of Computer Science, University of Waterloo, 1972)
↑ Gérard Huet: A Unification Algorithm for typed Lambda-Calculus []
↑ Gérard Huet: Higher Order Unification 30 Years Later
↑ Gilles Dowek: Higher-Order Unification and Matching. Handbook of Automated Reasoning 2001: 1009–1062
↑ Miller, Dale (1991). "लैम्ब्डा-एब्स्ट्रैक्शन, फंक्शन वेरिएबल्स और सरल एकीकरण के साथ एक लॉजिक प्रोग्रामिंग भाषा" (PDF). Journal of Logic and Computation. 1 (4): 497–536. doi:10.1093/logcom/1.4.497.
↑ Libal, Tomer; Miller, Dale (May 2022). "Functions-as-constructors higher-order unification: extended pattern unification". Annals of Mathematics and Artificial Intelligence. 90 (5): 455–479. doi:10.1007/s10472-021-09774-y.
↑ Gardent, Claire; Kohlhase, Michael; Konrad, Karsten (1997). "A Multi-Level, Higher-Order Unification Approach to Ellipsis". Submitted to European Association for Computational Linguistics (EACL). CiteSeerX 10.1.1.55.9018.
↑ Wayne Snyder (Jul 1990). "Higher order E-unification". प्रोक. स्वचालित कटौती पर 10वां सम्मेलन. LNAI. Vol. 449. Springer. pp. 573–587.

अग्रिम पठन

Franz Baader and Wayne Snyder (2001). "Unification Theory" Archived 2015-06-08 at the Wayback Machine. In John Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning, volume I, pages 447–533. Elsevier Science Publishers.^{[dead link]}
Gilles Dowek (2001). "Higher-order Unification and Matching". In Handbook of Automated Reasoning.
Franz Baader and Tobias Nipkow (1998). Term Rewriting and All That. Cambridge University Press.
Franz Baader and Jörg H. Siekmann [de] (1993). "Unification Theory". In Handbook of Logic in Artificial Intelligence and Logic Programming.
Jean-Pierre Jouannaud and Claude Kirchner (1991). "Solving Equations in Abstract Algebras: A Rule-Based Survey of Unification". In Computational Logic: Essays in Honor of Alan Robinson.
Nachum Dershowitz and Jean-Pierre Jouannaud, Rewrite Systems, in: Jan van Leeuwen (ed.), Handbook of Theoretical Computer Science, volume B Formal Models and Semantics, Elsevier, 1990, pp. 243–320
Jörg H. Siekmann (1990). "Unification Theory". In Claude Kirchner (editor) Unification. Academic Press.
Kevin Knight (Mar 1989). "Unification: A Multidisciplinary Survey" (PDF). ACM Computing Surveys. 21 (1): 93–124. CiteSeerX 10.1.1.64.8967. doi:10.1145/62029.62030. S2CID 14619034.
Gérard Huet and Derek C. Oppen (1980). "Equations and Rewrite Rules: A Survey". Technical report. Stanford University.
Raulefs, Peter; Siekmann, Jörg; Szabó, P.; Unvericht, E. (1979). "A short survey on the state of the art in matching and unification problems". ACM SIGSAM Bulletin. 13 (2): 14–20. doi:10.1145/1089208.1089210. S2CID 17033087.
Claude Kirchner and Hélène Kirchner. Rewriting, Solving, Proving. In preparation.

[6] E.g. a ⊕ (b ⊕ f(x)) ≡ a ⊕ (f(x) ⊕ b) ≡ (b ⊕ f(x)) ⊕ a ≡ (f(x) ⊕ b) ⊕ a

[7] since $(x\oplus y)\{x\mapsto z,y\mapsto z\}=z\oplus z\equiv z$

[8] since $z {z \mapsto x \oplus y} = x \oplus y$

[13] rmally: each unifier τ satisfies $\forall x : xτ = (xσ) ρ$ for some substitution ρ

[17] Alg.1, p.261. Their rule (a) corresponds to rule swap here, (b) to delete, (c) to both decompose and conflict, and (d) to both eliminate and check.

[25] Independent discovery is stated in Martelli, Montanari (1982),^[9] sect.1, p.259. Paterson's and Wegman's journal paper^[16] is dated 1978; however, the journal publisher received it in Sep.1976.

[26] Although the rule keeps x ≐ t in G, it cannot loop forever since its precondition x∈vars(G) is invalidated by its first application. More generally, the algorithm is guaranteed to terminate always, see below.

[LRequivC-37] 8.0 ^8.1 in the presence of equality $C$ , equalities $N l$ and $N r$ are equivalent, similar for $D l$ and $D r$

[1] J. Herbrand: Recherches sur la théorie de la démonstration. Travaux de la société des Sciences et des Lettres de Varsovie, Class III, Sciences Mathématiques et Physiques, 33, 1930.

[2] Claus-Peter Wirth; Jörg Siekmann; Christoph Benzmüller; Serge Autexier (2009). एक तर्कशास्त्री के रूप में जैक्स हेरब्रांड पर व्याख्यान (SEKI Report). DFKI. arXiv:0902.4682. Here: p.56

[3] Jacques Herbrand (1930). Recherches sur la théorie de la demonstration (PDF) (Ph.D. thesis). A. Vol. 1252. Université de Paris. Here: p.96-97

[Robinson.1965-4] 4.0 ^4.1 ^4.2 ^4.3 J.A. Robinson (Jan 1965). "संकल्प सिद्धांत पर आधारित एक मशीन-उन्मुख तर्क". Journal of the ACM. 12 (1): 23–41. doi:10.1145/321250.321253. S2CID 14389185.; Here: sect.5.8, p.32

[5] J.A. Robinson (1971). "Computational logic: The unification computation". Machine Intelligence. 6: 63–72.

[Vukmirovic-9] 6.0 ^6.1 ^6.2 Vukmirović, Petar; Bentkamp, Alexander; Nummelin, Visa (14 December 2021). "कुशल पूर्ण उच्च-क्रम एकीकरण". Logical Methods in Computer Science. 17 (4): 6919. doi:10.46298/lmcs-17(4:18)2021.

[10] Apt, Krzysztof R. (1997). लॉजिक प्रोग्रामिंग से लेकर प्रोलॉग तक (1. publ ed.). London Munich: Prentice Hall. p. 24. ISBN 013230368X.

[11] Fages, François; Huet, Gérard (1986). "समीकरण सिद्धांतों में यूनिफायर और मैचर्स का पूरा सेट". Theoretical Computer Science. 43: 189–200. doi:10.1016/0304-3975(86)90175-1.

[Martelli.Montanari.1982-12] 9.0 ^9.1 ^9.2 Martelli, Alberto; Montanari, Ugo (Apr 1982). "एक कुशल एकीकरण एल्गोरिदम". ACM Trans. Program. Lang. Syst. 4 (2): 258–282. doi:10.1145/357162.357169. S2CID 10921306.

[14] Robinson (1965);^[4] nr.2.5, 2.14, p.25

[15] Robinson (1965);^[4] nr.5.6, p.32

[16] Robinson (1965);^[4] nr.5.8, p.32

[18] Lewis Denver Baxter (Feb 1976). एक व्यावहारिक रूप से रैखिक एकीकरण एल्गोरिदम (PDF) (Res. Report). Vol. CS-76-13. Univ. of Waterloo, Ontario.

[19] Gérard Huet (Sep 1976). Resolution d'Equations dans des Langages d'Ordre 1,2,...ω (These d'etat). Universite de Paris VII.

[Martelli.Montanari.1976-20] 15.0 ^15.1 Alberto Martelli & Ugo Montanari (Jul 1976). Unification in linear time and space: A structured presentation (Internal Note). Vol. IEI-B76-16. Consiglio Nazionale delle Ricerche, Pisa. Archived from the original on 2015-01-15.

[Paterson.Wegman.1978-21] 16.0 ^16.1 ^16.2 ^16.3 Michael Stewart Paterson and M.N. Wegman (Apr 1978). "रैखिक एकीकरण". J. Comput. Syst. Sci. 16 (2): 158–167. doi:10.1016/0022-0000(78)90043-0.

[22] J.A. Robinson (Jan 1976). "Fast unification". In Woodrow W. Bledsoe, Michael M. Richter (ed.). प्रोक. प्रमेय सिद्ध करने की कार्यशाला ओबेरवुल्फ़च. Oberwolfach Workshop Report. Vol. 1976/3.^{[permanent dead link]}

[23] M. Venturini-Zilli (Oct 1975). "प्रथम-क्रम अभिव्यक्तियों के लिए एकीकरण एल्गोरिथ्म की जटिलता". Calcolo. 12 (4): 361–372. doi:10.1007/BF02575754. S2CID 189789152.

[24] Paterson, M.S.; Wegman, M.N. (May 1976). Chandra, Ashok K.; Wotschke, Detlef; Friedman, Emily P.; Harrison, Michael A. (eds.). रैखिक एकीकरण. Proceedings of the eighth annual ACM Symposium on Theory of Computing (STOC). ACM. pp. 181–186. doi:10.1145/800113.803646.

[27] McBride, Conor (October 2003). "संरचनात्मक प्रत्यावर्तन द्वारा प्रथम-क्रम एकीकरण". Journal of Functional Programming. 13 (6): 1061–1076. CiteSeerX 10.1.1.25.1516. doi:10.1017/S0956796803004957. ISSN 0956-7968. S2CID 43523380. Retrieved 30 March 2012.

[28] .g. Paterson, Wegman (1978),^[16] sect.2, p.159

[29] Jonathan Calder, Mike Reape, and Hank Zeevat,, An algorithm for generation in unification categorial grammar. In Proceedings of the 4th Conference of the European Chapter of the Association for Computational Linguistics, pages 233-240, Manchester, England (10–12 April), University of Manchester Institute of Science and Technology, 1989.

[30] Graeme Hirst and David St-Onge, [1] Lexical chains as representations of context for the detection and correction of malapropisms, 1998.

[31] Walther, Christoph (1985). "कई-क्रमबद्ध रिज़ॉल्यूशन द्वारा शुबर्ट के स्टीमरोलर का एक यांत्रिक समाधान" (PDF). Artif. Intell. 26 (2): 217–224. doi:10.1016/0004-3702(85)90029-3. Archived from the original (PDF) on 2011-07-08. Retrieved 2013-06-28.

[32] Smolka, Gert (Nov 1988). पॉलिमॉर्फिकली ऑर्डर-सॉर्टेड प्रकारों के साथ लॉजिक प्रोग्रामिंग (PDF). Int. Workshop Algebraic and Logic Programming. LNCS. Vol. 343. Springer. pp. 53–70. doi:10.1007/3-540-50667-5_58.

[33] Schmidt-Schauß, Manfred (Apr 1988). टर्म घोषणाओं के साथ ऑर्डर-सॉर्टेड लॉजिक के कम्प्यूटेशनल पहलू. Lecture Notes in Artificial Intelligence (LNAI). Vol. 395. Springer.

[34] Gordon D. Plotkin, Lattice Theoretic Properties of Subsumption, Memorandum MIP-R-77, Univ. Edinburgh, Jun 1970

[35] Mark E. Stickel, A Unification Algorithm for Associative-Commutative Functions, J. Assoc. Comput. Mach., vol.28, no.3, pp. 423–434, 1981

[Fages.1987-36] 29.0 ^29.1 F. Fages, Associative-Commutative Unification, J. Symbolic Comput., vol.3, no.3, pp. 257–275, 1987

[38] Franz Baader, Unification in Idempotent Semigroups is of Type Zero, J. Automat. Reasoning, vol.2, no.3, 1986

[39] J. Makanin, The Problem of Solvability of Equations in a Free Semi-Group, Akad. Nauk SSSR, vol.233, no.2, 1977

[40] F. Fages (1987). "साहचर्य-अनुकरणीय एकीकरण" (PDF). J. Symbolic Comput. 3 (3): 257–275. doi:10.1016/s0747-7171(87)80004-4.

[41] Martin, U., Nipkow, T. (1986). "Unification in Boolean Rings". In Jörg H. Siekmann (ed.). Proc. 8th CADE. LNCS. Vol. 230. Springer. pp. 506–513.{{cite book}}: CS1 maint: multiple names: authors list (link)

[42] A. Boudet; J.P. Jouannaud; M. Schmidt-Schauß (1989). "बूलियन रिंग्स और एबेलियन समूहों का एकीकरण". Journal of Symbolic Computation. 8 (5): 449–477. doi:10.1016/s0747-7171(89)80054-9.

[Baader_and_Snyder_2001,_p._486-43] 35.0 ^35.1 Baader and Snyder (2001), p. 486.

[44] F. Baader and S. Ghilardi, Unification in modal and description logics, Logic Journal of the IGPL 19 (2011), no. 6, pp. 705–730.

[45] P. Szabo, Unifikationstheorie erster Ordnung (First Order Unification Theory), Thesis, Univ. Karlsruhe, West Germany, 1982

[46] Jörg H. Siekmann, Universal Unification, Proc. 7th Int. Conf. on Automated Deduction, Springer LNCS vol.170, pp. 1–42, 1984

[47] N. Dershowitz and G. Sivakumar, Solving Goals in Equational Languages, Proc. 1st Int. Workshop on Conditional Term Rewriting Systems, Springer LNCS vol.308, pp. 45–55, 1988

[48] Fay (1979). "First-Order Unification in an Equational Theory". Proc. 4th Workshop on Automated Deduction. pp. 161–167.

[Goldfarb.1981-49] 41.0 ^41.1 Warren D. Goldfarb (1981). "द्वितीय-क्रम एकीकरण समस्या की अनिर्णयता". TCS. 13 (2): 225–230. doi:10.1016/0304-3975(81)90040-2.

[50] Gérard P. Huet (1973). "तीसरे क्रम के तर्क में एकीकरण की अनिश्चितता". Information and Control. 22 (3): 257–267. doi:10.1016/S0019-9958(73)90301-X.

[51] Claudio Lucchesi: The Undecidability of the Unification Problem for Third Order Languages (Research Report CSRR 2059; Department of Computer Science, University of Waterloo, 1972)

[52] Gérard Huet: A Unification Algorithm for typed Lambda-Calculus []

[53] Gérard Huet: Higher Order Unification 30 Years Later

[54] Gilles Dowek: Higher-Order Unification and Matching. Handbook of Automated Reasoning 2001: 1009–1062

[55] Miller, Dale (1991). "लैम्ब्डा-एब्स्ट्रैक्शन, फंक्शन वेरिएबल्स और सरल एकीकरण के साथ एक लॉजिक प्रोग्रामिंग भाषा" (PDF). Journal of Logic and Computation. 1 (4): 497–536. doi:10.1093/logcom/1.4.497.

[56] Libal, Tomer; Miller, Dale (May 2022). "Functions-as-constructors higher-order unification: extended pattern unification". Annals of Mathematics and Artificial Intelligence. 90 (5): 455–479. doi:10.1007/s10472-021-09774-y.

[57] Gardent, Claire; Kohlhase, Michael; Konrad, Karsten (1997). "A Multi-Level, Higher-Order Unification Approach to Ellipsis". Submitted to European Association for Computational Linguistics (EACL). CiteSeerX 10.1.1.55.9018.

[58] Wayne Snyder (Jul 1990). "Higher order E-unification". प्रोक. स्वचालित कटौती पर 10वां सम्मेलन. LNAI. Vol. 449. Springer. pp. 573–587.

[1]

[2]

[3]

[4]

[5]

[note 1]

[note 2]

[note 3]

[6]

[7]

[8]

[9]

[note 4]

[10]

[11]

[12]

[note 5]

[13]

[14]

[15]

[16]

[17]

[18]

[19]

[note 6]

[note 7]

[20]

[21]

[22]

[23]

[24]

[25]

[26]

[27]

[28]

[29]

[note 8]

[30]

[31]

[32]

[33]

[34]

[35]

[36]

[37]

[38]

[39]

[40]

[41]

[42]

[43]

[44]

[45]

[46]

[47]

[48]

[49]

[50]

Anonymous

Search

एकीकरण (कंप्यूटर विज्ञान): Difference between revisions

Namespaces

More

Page actions

Latest revision as of 11:05, 12 August 2023

Contents

फॉर्मल परिभाषा

प्रिरेक्विज़िट

प्रतिस्थापन

सामान्यीकरण, विशेषज्ञता

हल समुच्चय

प्रथम-क्रम शब्दों का वाक्यात्मकएकीकरण

एक एकीकरण कलन विधि

ओक्कुर चेक

समाप्ति का प्रमाण

प्रथम-क्रम शब्दों के वाक्यात्मकएकीकरण के उदाहरण

अनुप्रयोग: लॉजिक प्रोग्रामिंग में एकीकरण

अनुप्रयोग: प्रकार अनुमान

अनुप्रयोग: फ़ीचर संरचना एकीकरण

क्रमानुसार एकीकरण

अनंत पदों का एकीकरण

ई-एकीकरण

विशेष पृष्ठभूमि ज्ञान समुच्चय E

एकतरफा पैरामोड्यूलेशन

संकुचन

उच्च-क्रम एकीकरण

यह भी देखें

टिप्पणियाँ

संदर्भ

अग्रिम पठन

Navigation

Navigation

Wiki tools

Wiki tools

@@ Line 1: / Line 1: @@
-[[तर्क|लॉजिक]] और [[कंप्यूटर विज्ञान]] में यूनिफिकेशन सिंबॉलिक [[अभिव्यक्ति (गणित)|एक्सप्रेशन (गणित)]] के बीच समीकरणों को हल करने की कलनविधि प्रक्रिया का उपयोग किया जाता है। उदाहरण के लिए x,y,z को चर के रूप में उपयोग करते हुए सिंगलटन समीकरण सेट { ''[[cons]]''(''x'',''cons''(''x'',''nil'')) = ''cons''(2,''y'') } एक सिंटैक्टिक प्रथम-क्रम यूनिफिकेशन समस्या के रूप में है, जिसके पास प्रतिस्थापन {''x'' ↦ 2, ''y'' ↦ ''cons''(2,''nil'') } का एकमात्र सलूशन होता है।
+[[तर्क|लॉजिक]] और [[कंप्यूटर विज्ञान]] में '''एकीकरण''' सिंबॉलिक [[अभिव्यक्ति (गणित)|अभिव्यक्तियों (गणित)]] के बीच समीकरणों को हल करने के लिए कलन विधि प्रक्रिया का उपयोग किया जाता है। उदाहरण के लिए x,y,z को चर के रूप में उपयोग करते हुए एकल समीकरण समुच्चय { ''[[cons]]''(''x'',''cons''(''x'',''nil'')) = ''cons''(2,''y'') } एक वाक्यात्मक प्रथम-क्रम एकीकरण समस्या के रूप में है, जिसके पास प्रतिस्थापन {''x'' ↦ 2, ''y'' ↦ ''cons''(2,''nil'') } के रूप में एकमात्र हल होता है।
-यूनिफिकेशन कलनविधि की खोज सबसे पहले [[जैक्स हेरब्रांड]] ने की थी,<ref>J. Herbrand: Recherches sur la théorie de la démonstration. ''Travaux de la société des Sciences et des Lettres de Varsovie'', Class III, Sciences Mathématiques et Physiques, 33, 1930.</ref><ref>{{cite report | author1=Claus-Peter Wirth |  author2=Jörg Siekmann | author3= Christoph Benzmüller | author4= Serge Autexier | title=एक तर्कशास्त्री के रूप में जैक्स हेरब्रांड पर व्याख्यान| institution=DFKI | type=SEKI Report | number=SR-2009-01 | year=2009 | arxiv=0902.4682 }} Here: p.56</ref><ref>{{cite thesis | type=Ph.D. thesis | url=http://www.numdam.org/issue/THESE_1930__110__1_0.pdf | author=Jacques Herbrand | title=Recherches sur la théorie de la demonstration | institution=Université de Paris | series=A | volume=1252 | year=1930 }} Here: p.96-97</ref> जबकि पहली फॉर्मल जांच का श्रेय [[जॉन एलन रॉबिन्सन]] को दिया जाता है,<ref name="Robinson.1965">{{cite journal | author=J.A. Robinson | title=संकल्प सिद्धांत पर आधारित एक मशीन-उन्मुख तर्क| journal=Journal of the ACM | volume=12 | number=1 | pages=23–41 |date=Jan 1965 | doi=10.1145/321250.321253| s2cid=14389185 }}; Here: sect.5.8, p.32</ref><ref>{{cite journal | author=J.A. Robinson | title=Computational logic: The unification computation | journal=Machine Intelligence | volume=6 | pages=63–72 | url=https://aitopics.org/download/classics:E35191E8 | year=1971 }}</ref> जिन्होंने प्रथम-क्रम लॉजिक के लिए अपने सलूशन प्रक्रिया के मौलिक निर्माण खंड के रूप में प्रथम-क्रम सिंटैक्टिक यूनिफिकेशन का उपयोग किया जाता है, इस प्रकार [[स्वचालित तर्क|स्वचालित लॉजिक को]] प्रौद्योगिकी में एक बड़ा कदम के रूप में आगे माना जाता है, क्योंकि इसने संयोजन विस्फोट के एक स्रोत को समाप्त कर दिया था। यह संयोजक के रूप में आज भी एक स्रोत बन गया है और इसे स्वचालित लॉजिक यूनिफिकेशन का मुख्य क्षेत्र माना जाता है। सिंटैक्टिक प्रथम-क्रम यूनिफिकेशन का उपयोग [[तर्क प्रोग्रामिंग|लॉजिक प्रोग्रामिंग]] और प्रोग्रामिंग लैंग्वेज [[प्रकार प्रणाली|टाइप प्रणाली]] कार्यान्वयन के रूप में किया जाता है और इस प्रकार विशेष रूप से हिंडले-मिलनर आधारित टाइप अनुमान कलनविधि के रूप में होता है। सिमेंटिक यूनिफिकेशन का उपयोग एसएमटी सॉल्वर्स, [[शब्द पुनर्लेखन]] कलनविधि और [[क्रिप्टोग्राफ़िक प्रोटोकॉल|क्रिप्टोआलेख़िक प्रोटोकॉल]] विश्लेषण के रूप में किया जाता है। उच्च-क्रम यूनिफिकेशन का उपयोग प्रूफ़ सहायकों के रूप में किया जाता है, उदाहरण के लिए इसाबेल और [[बारह|ट्वेल्व]] और उच्च-क्रम यूनिफिकेशन के प्रतिबंधित रूपों का उपयोग कुछ प्रोग्रामिंग लैंग्वेज कार्यान्वयन के रूप में किया जाता है, चूकि कुछ प्रोग्रामिंग [[लैम्डैप्रोलॉग]] के सीमित रूपों का उपयोग किया जाता है, क्योंकि उच्च-क्रम पैटर्न इक्स्प्रेसिव के रूप में होते हैं, फिर भी उनकी संबद्ध यूनिफिकेशन प्रक्रिया सैद्धांतिक गुणों को प्रथम-क्रम यूनिफिकेशन के रूप में निकटता बनाए रखती है।
+एकीकरण कलन विधि की खोज सबसे पहले [[जैक्स हेरब्रांड]] ने की थी,<ref>J. Herbrand: Recherches sur la théorie de la démonstration. ''Travaux de la société des Sciences et des Lettres de Varsovie'', Class III, Sciences Mathématiques et Physiques, 33, 1930.</ref><ref>{{cite report | author1=Claus-Peter Wirth |  author2=Jörg Siekmann | author3= Christoph Benzmüller | author4= Serge Autexier | title=एक तर्कशास्त्री के रूप में जैक्स हेरब्रांड पर व्याख्यान| institution=DFKI | type=SEKI Report | number=SR-2009-01 | year=2009 | arxiv=0902.4682 }} Here: p.56</ref><ref>{{cite thesis | type=Ph.D. thesis | url=http://www.numdam.org/issue/THESE_1930__110__1_0.pdf | author=Jacques Herbrand | title=Recherches sur la théorie de la demonstration | institution=Université de Paris | series=A | volume=1252 | year=1930 }} Here: p.96-97</ref> जबकि पहली फॉर्मल जांच का श्रेय [[जॉन एलन रॉबिन्सन]] को दिया जाता है,<ref name="Robinson.1965">{{cite journal | author=J.A. Robinson | title=संकल्प सिद्धांत पर आधारित एक मशीन-उन्मुख तर्क| journal=Journal of the ACM | volume=12 | number=1 | pages=23–41 |date=Jan 1965 | doi=10.1145/321250.321253| s2cid=14389185 }}; Here: sect.5.8, p.32</ref><ref>{{cite journal | author=J.A. Robinson | title=Computational logic: The unification computation | journal=Machine Intelligence | volume=6 | pages=63–72 | url=https://aitopics.org/download/classics:E35191E8 | year=1971 }}</ref> जिन्होंने प्रथम-क्रम लॉजिक के लिए अपने हल प्रक्रिया के मौलिक निर्माण खंड के रूप में प्रथम-क्रम वाक्यात्मक एकीकरण का उपयोग किया है, इस प्रकार [[स्वचालित तर्क|स्वचालित लॉजिक को]] प्रौद्योगिकी में एक बड़े कदम के रूप में माना जाता है, क्योंकि इसने संयोजन विस्फोट के एक स्रोत को समाप्त कर दिया था। यह संयोजक के रूप में आज भी एक स्रोत बन गया है और इसे स्वचालित लॉजिक एकीकरण का मुख्य क्षेत्र माना जाता है। वाक्यात्मक प्रथम-क्रम एकीकरण का उपयोग [[तर्क प्रोग्रामिंग|लॉजिक प्रोग्रामिंग]] और प्रोग्रामिंग लैंग्वेज [[प्रकार प्रणाली|टाइप प्रणाली]] कार्यान्वयन के रूप में किया जाता है और इस प्रकार विशेष रूप से हिंडले-मिलनर आधारित टाइप अनुमान कलन विधि के रूप में होता है। सिमेंटिक एकीकरण का उपयोग एसएमटी सॉल्वर्स, [[शब्द पुनर्लेखन]] कलन विधि और [[क्रिप्टोग्राफ़िक प्रोटोकॉल|क्रिप्टोआलेख़िक प्रोटोकॉल]] विश्लेषण के रूप में किया जाता है। उच्च-क्रम एकीकरण का उपयोग प्रूफ़ सहायकों के रूप में किया जाता है। उदाहरण के लिए इसाबेल और [[बारह|ट्वेल्व]] और उच्च-क्रम एकीकरण के प्रतिबंधित रूपों का उपयोग कुछ प्रोग्रामिंग लैंग्वेज कार्यान्वयन के रूप में किया जाता है, चूकि कुछ प्रोग्रामिंग [[लैम्डैप्रोलॉग]] के सीमित रूपों का उपयोग किया जाता है, क्योंकि उच्च-क्रम पैटर्न इक्स्प्रेसिव के रूप में होते हैं, फिर भी उनकी संबद्ध एकीकरण प्रक्रिया सैद्धांतिक गुणों को प्रथम-क्रम एकीकरण के रूप में निकटता बनाए रखती है।
 =='''फॉर्मल परिभाषा''' ==
-यूनिफिकेशन समस्या एक सीमित समुच्चय के रूप में है {{math|1=''E''={{mset| ''l''<sub>1</sub> ≐ ''r''<sub>1</sub>, ..., ''l''<sub>''n''</sub> ≐ ''r''<sub>''n''</sub> }}}} समीकरणों को हल करना है, जहाँ {{math|''l''<sub>''i''</sub>, ''r''<sub>''i''</sub>}} सेट में हैं <math>T</math> शब्दों या एक्सप्रेशन का. समीकरण सेट या यूनिफिकेशन समस्या में किन एक्सप्रेशन या शब्दों को घटित होने की अनुमति दी जाती है और किस एक्सप्रेशन को समान माना जाता है, इसके आधार पर यूनिफिकेशन के रूप में कई ढांचे प्रतिष्ठित हैं। यदि उच्च-क्रम वाले चर अर्थात [[फ़ंक्शन (गणित)|फलन (गणित)]] का प्रतिनिधित्व करने वाले चर, को एक एक्सप्रेशन में अनुमति दी जाती है, तो प्रक्रिया को 'उच्च-क्रम एकीकरण' कहा जाता है, अन्यथा 'प्रथम-क्रम एकीकरण' का रूप कहा जाता है। यदि प्रत्येक समीकरण के दोनों पक्षों को वस्तुतः समान बनाने के लिए किसी सलूशन की आवश्यकता होती है, तो प्रक्रिया को 'वाक्यविन्यास' या 'मुक्त एकीकरण' कहा जाता है, अन्यथा सिमेंटिक या 'समीकरणात्मक यूनिफिकेशन या ई-यूनिफिकेशन या यूनिफिकेशन मॉड्यूलो सिद्धांत कहा जाता है।
+एकीकरण समस्या हल करने के लिए समीकरणों का एक सीमित समुच्चय {{math|1=''E''={{mset| ''l''<sub>1</sub> ≐ ''r''<sub>1</sub>, ..., ''l''<sub>''n''</sub> ≐ ''r''<sub>''n''</sub> }}}} के रूप में होता है, जहाँ {{math|''l''<sub>''i''</sub>, ''r''<sub>''i''</sub>}} पदों या अभिव्यक्तियों के समुच्चय <math>T</math> के रूप में होता हैं। समीकरण समुच्चय या एकीकरण समस्या में किन अभिव्यक्तियों या शब्दों को घटित होने की अनुमति होती है और किन अभिव्यक्तियों को समान माना जाता है, इसके आधार पर एकीकरण के रूप में कई ढांचे प्रतिष्ठित हैं। यदि उच्च-क्रम वाले चर अर्थात [[फ़ंक्शन (गणित)|फलन (गणित)]] का प्रतिनिधित्व करने वाले चर को एक अभिव्यक्तियों में अनुमति होती है, तो प्रक्रिया को 'उच्च-क्रम एकीकरण' कहा जाता है। अन्यथा 'प्रथम-क्रम एकीकरण' का रूप कहा जाता है। यदि प्रत्येक समीकरण के दोनों पक्षों को वस्तुतः समान बनाने के लिए किसी समाधान की आवश्यकता होती है, तो प्रक्रिया को 'वाक्यविन्यास' या 'मुक्त एकीकरण' कहा जाता है, अन्यथा सिमेंटिक या 'समीकरणात्मक एकीकरण या ई- एकीकरण या एकीकरण मॉड्यूलो सिद्धांत कहा जाता है।
-यदि प्रत्येक समीकरण का दाहिना भाग बंद है, को E मुक्त चर नहीं है, तो समस्या को पैटर्न मिलान कहा जाता है। प्रत्येक समीकरण के बाईं ओर चर के साथ पैटर्न का रूप कहा जाता है।<ref>{{cite book |last1=Dowek |first1=Gilles |title=स्वचालित तर्क की पुस्तिका|date=1 January 2001 |publisher=Elsevier Science Publishers B. V. |isbn=978-0-444-50812-6 |pages=1009–1062 |url=http://www.lsv.fr/~dowek/Publi/unification.ps |chapter=Higher-order unification and matching}}</ref>
 === '''प्रिरेक्विज़िट''' ===
-फॉर्मल रूप से, एक यूनिफिकेशन दृष्टिकोण का अनुमान लगाया जाता है
+औपचारिक रूप से एक एकीकरण दृष्टिकोण का अनुमान लगाया जाता है
-* एक अनंत समुच्चय <math>V</math> चर का. उच्च-क्रम यूनिफिकेशन के लिए, इसे चुनना सुविधाजनक है <math>V</math> [[लैम्ब्डा-टर्म बाध्य चर]] के सेट से भिन्न हो जाता है।
+* एक अनंत समुच्चय <math>V</math> चर का. उच्च-क्रम एकीकरण के लिए, इसे चुनना सुविधाजनक है <math>V</math> [[लैम्ब्डा-टर्म बाध्य चर]] के समुच्चय से भिन्न हो जाता है।
-* एक सेट <math>T</math> ऐसे शब्दों का <math>V \subseteq T</math>. प्रथम-क्रम यूनिफिकेशन के लिए, <math>T</math> सामान्यतः प्रथम-क्रम शब्दों चर और फलन प्रतीकों से निर्मित शब्द का सेट होता है। उच्च-क्रम यूनिफिकेशन के लिए <math>T</math> इसमें प्रथम-क्रम वाले शब्द और लैम्ब्डा शब्द कुछ उच्च-क्रम वाले चर वाले शब्द के रूप में सम्मिलित होते हैं।
+* एक समुच्चय <math>T</math> ऐसे शब्दों का <math>V \subseteq T</math>. प्रथम-क्रम एकीकरण के लिए, <math>T</math> सामान्यतः प्रथम-क्रम शब्दों चर और फलन प्रतीकों से निर्मित शब्द का समुच्चय होता है। उच्च-क्रम एकीकरण के लिए <math>T</math> इसमें प्रथम-क्रम वाले शब्द और लैम्ब्डा शब्द कुछ उच्च-क्रम वाले चर वाले शब्द के रूप में सम्मिलित होते हैं।
-* एक मैपिंग संस्करण: <math>T \rightarrow</math> पावर सेट|<math>\mathbb{P}</math><math>(V)</math>, प्रत्येक पद को निर्दिष्ट करना <math>t</math> सेट <math>\text{vars}(t) \subsetneq V</math> में होने वाले मुक्त चर के रूप में <math>t</math> होता है.
+* एक मैपिंग संस्करण: <math>T \rightarrow</math> पावर समुच्चय |<math>\mathbb{P}</math><math>(V)</math>, प्रत्येक पद को निर्दिष्ट करना <math>t</math> समुच्चय <math>\text{vars}(t) \subsetneq V</math> में होने वाले मुक्त चर के रूप में <math>t</math> होता है.
-* एक सिद्धांत या तुल्यता संबंध <math>\equiv</math> पर <math>T</math>, यह दर्शाता है कि कौन से पद समान माने जाते हैं। प्रथम-क्रम ई-यूनिफिकेशन के लिए, <math>\equiv</math> कुछ फलन प्रतीकों के बारे में पृष्ठभूमि ज्ञान को दर्शाता है; उदाहरण के लिए, यदि <math>\oplus</math> क्रमविनिमेय माना जाता है, <math>t\equiv u</math> यदि <math>u</math> वहां से परिणाम मिले <math>t</math> के लॉजिक ों की अदला-बदली करके <math>\oplus</math> कुछ संभवतः सभी घटनाओं पर। <ref group=note>E.g. ''a'' ⊕ (''b'' ⊕ ''f''(''x'')) ≡ ''a'' ⊕ (''f''(''x'') ⊕ ''b'') ≡ (''b'' ⊕ ''f''(''x'')) ⊕ ''a'' ≡ (''f''(''x'') ⊕ ''b'') ⊕ ''a''</ref> सबसे विशिष्ट स्थिति में जब कोई पृष्ठभूमि ज्ञान नहीं होता है, तो मात्र शाब्दिक रूप से या सिंटैक्टिक रूप से समान शब्दों को समान माना जाता है। इस स्थिति में ≡ को [[मुक्त सिद्धांत]] कहा जाता है, क्योंकि यह एक स्वतंत्र वस्तु के रूप में है, खाली सिद्धांत क्योंकि समीकरण [[वाक्य (गणितीय तर्क)|वाक्य (गणितीय लॉजिक )]] का सेट या पृष्ठभूमि ज्ञान के रूप में खाली है), [[अव्याख्यायित कार्य|अव्याख्यायित कार्यों]] का सिद्धांत पर किया जाता है, क्योंकि यूनिफिकेशन अनिर्वचनीय [[शब्द (तर्क)|शब्द (लॉजिक )]]) या बीजगणितीय विनिर्देश के सिद्धांत के रूप में किया जाता है, क्योंकि सभी फलन प्रतीक मात्र उन पर काम करने के अतिरिक्त डेटा शब्द के रूप में बनाते हैं। सामान्यतः उच्च-क्रम यूनिफिकेशन के लिए <math>t\equiv u</math> यदि <math>t</math> और <math>u</math> अल्फ़ा समतुल्य होता है.
+* एक सिद्धांत या तुल्यता संबंध <math>\equiv</math> पर <math>T</math>, यह दर्शाता है, कि कौन से पद समान माने जाते हैं। प्रथम-क्रम ई- एकीकरण के लिए, <math>\equiv</math> कुछ फलन प्रतीकों के बारे में पृष्ठभूमि ज्ञान को दर्शाता है; उदाहरण के लिए, यदि <math>\oplus</math> क्रमविनिमेय माना जाता है, <math>t\equiv u</math> यदि <math>u</math> वहां से परिणाम मिले <math>t</math> के लॉजिक की अदला-बदली करके <math>\oplus</math> कुछ संभवतः सभी घटनाओं पर। <ref group=note>E.g. ''a'' ⊕ (''b'' ⊕ ''f''(''x'')) ≡ ''a'' ⊕ (''f''(''x'') ⊕ ''b'') ≡ (''b'' ⊕ ''f''(''x'')) ⊕ ''a'' ≡ (''f''(''x'') ⊕ ''b'') ⊕ ''a''</ref> सबसे विशिष्ट स्थिति में जब कोई पृष्ठभूमि ज्ञान नहीं होता है, तो मात्र शाब्दिक रूप से या वाक्यात्मकरूप से समान शब्दों को समान माना जाता है। इस स्थिति में ≡ को [[मुक्त सिद्धांत]] कहा जाता है, क्योंकि यह एक स्वतंत्र वस्तु के रूप में है, खाली सिद्धांत क्योंकि समीकरण [[वाक्य (गणितीय तर्क)|वाक्य (गणितीय लॉजिक )]] का समुच्चय या पृष्ठभूमि ज्ञान के रूप में खाली है, [[अव्याख्यायित कार्य|अव्याख्यायित फलन]] के सिद्धांत पर किया जाता है, क्योंकि एकीकरण अनिर्वचनीय [[शब्द (तर्क)|शब्द (लॉजिक)]]) या बीजगणितीय विनिर्देश के सिद्धांत के रूप में किया जाता है, क्योंकि सभी फलन प्रतीक मात्र उन पर काम करने के अतिरिक्त डेटा शब्द के रूप में जाने जाते है। सामान्यतः उच्च-क्रम एकीकरण के लिए <math>t\equiv u</math> यदि <math>t</math> और <math>u</math> अल्फ़ा समतुल्य होता है.
-शब्दों और सिद्धांत का सेट समाधानों के सेट को कैसे प्रभावित करता है, इसके उदाहरण के रूप में सिंटैक्टिक प्रथम-क्रम यूनिफिकेशन समस्या { y = cons(2,y) } का परिमित शब्दों के सेट पर कोई सलूशन नहीं है। चूंकि, ट्री सेट सिद्धांत शर्तों के सेट पर इसका एकल सलूशन के रूप में { y ↦ cons(2,cons(2,cons(2,...)) } होता है। इसी प्रकार सिमेंटिक प्रथम-क्रम यूनिफिकेशन समस्या { a⋅x = x⋅a } में फॉर्म का प्रत्येक प्रतिस्थापन { x ↦ a⋅...⋅a } एक [[अर्धसमूह]] में सलूशन के रूप में होता है, अर्थात यदि (⋅) को साहचर्य माना जाता है, लेकिन वही समस्या जिसे [[एबेलियन समूह]] में देखा जाता है, जहां (⋅) को [[विनिमेय|क्रमविनिमेय]] भी माना जाता है, सलूशन के रूप में कोई भी प्रतिस्थापन होता है।
+शब्दों और सिद्धांत का समुच्चय समाधानों के समुच्चय को कैसे प्रभावित करता है, इसके उदाहरण के रूप में वाक्यात्मक प्रथम-क्रम एकीकरण समस्या { y = cons(2,y) } का परिमित शब्दों के समुच्चय पर कोई हल नहीं है। चूंकि, ट्री समुच्चय सिद्धांत शर्तों के समुच्चय पर इसका एकल हल के रूप में { y ↦ cons(2,cons(2,cons(2,...)) } होता है। इसी प्रकार सिमेंटिक प्रथम-क्रम एकीकरण समस्या { a⋅x = x⋅a } में फॉर्म का प्रत्येक प्रतिस्थापन { x ↦ a⋅...⋅a } एक [[अर्धसमूह]] में हल के रूप में होता है, अर्थात यदि (⋅) को साहचर्य माना जाता है, लेकिन वही समस्या जिसे [[एबेलियन समूह]] में देखा जाता है, जहां (⋅) को [[विनिमेय|क्रमविनिमेय]] के रूप में माना जाता है और इस प्रकार हल के रूप में कोई भी प्रतिस्थापन होता है
-उच्च-क्रम यूनिफिकेशन के उदाहरण के रूप में एकल सेट { a = y(x) } एक सिंटैक्टिक दूसरे क्रम की यूनिफिकेशन समस्या के रूप में होता है, क्योंकि y एक फलन चर है। एक सलूशन के रूप में है {x ↦ a, y ↦ (पहचान फलन) }; दूसरा है { y ↦ (निरंतर फलन प्रत्येक मान को a पर मैप करता है), x ↦ (को E भी मान) } होता है।
+उच्च-क्रम एकीकरण के उदाहरण के रूप में एकल समुच्चय { a = y(x) } एक वाक्यात्मक दूसरे क्रम की एकीकरण समस्या के रूप में होता है, क्योंकि y एक फलन चर है। एक हल x ↦ a, y ↦ आइडेंटिटी फलन) } है, इस प्रकार दूसरा { y ↦ निरंतर फलन है, जो प्रत्येक मान को a, x ↦ को किसी भी मान पर मैप करता है।
 ==='''प्रतिस्थापन'''===
 {{main|प्रतिस्थापन (लॉजिक)}}
-प्रतिस्थापन एक मानचित्रण है <math>\sigma: V\rightarrow T</math> चर से पदों तक; संकेतन <math> \{x_1\mapsto t_1, ..., x_k \mapsto t_k\}</math> प्रत्येक चर के रूप में प्रतिस्थापन मानचित्रण को संदर्भित करता है <math>x_i</math> पद के लिए <math>t_i</math>, के लिए <math>i=1,...,k</math>, और प्रत्येक अन्य चर स्वयं के लिए होता है। उस प्रतिस्थापन को किसी पद पर लागू करना <math>t</math> [[ उपसर्ग संकेतन |उपसर्ग संकेतन]] में इस प्रकार लिखा गया है <math>t \{x_1 \mapsto t_1, ..., x_k \mapsto t_k\}</math>; इसका अर्थ है (एक साथ) प्रत्येक चर की प्रत्येक घटना को प्रतिस्थापित करना <math>x_i</math> अवधि में <math>t</math> द्वारा <math>t_i</math>. परिणाम <math>t\tau</math> प्रतिस्थापन लागू करने का <math>\tau</math> एक पद के लिए <math>t</math> उस पद का उदाहरण कहा जाता है <math>t</math>.
+प्रतिस्थापन एक मानचित्रण है <math>\sigma: V\rightarrow T</math> चर से पदों तक; संकेतन <math> \{x_1\mapsto t_1, ..., x_k \mapsto t_k\}</math> प्रत्येक चर के रूप में प्रतिस्थापन मानचित्रण को संदर्भित करता है <math>x_i</math> पद के लिए <math>t_i</math>, के लिए <math>i=1,...,k</math>, और प्रत्येक अन्य चर स्वयं के लिए होता है। उस प्रतिस्थापन को किसी पद पर प्रयुक्त करना <math>t</math> [[ उपसर्ग संकेतन |उपसर्ग संकेतन]] में इस प्रकार लिखा गया है <math>t \{x_1 \mapsto t_1, ..., x_k \mapsto t_k\}</math>; इसका अर्थ है (एक साथ) प्रत्येक चर की प्रत्येक घटना को प्रतिस्थापित करना <math>x_i</math> अवधि में <math>t</math> द्वारा <math>t_i</math>. के रूप में होता है और इस प्रकार किसी पद <math>t</math>.में प्रतिस्थापन <math>t\tau</math> प्रयुक्त करने का परिणाम <math>\tau</math> उस पद पद के लिए <math>t</math> का उदाहरण कहलाता है। प्रथम-क्रम उदाहरण के रूप में प्रतिस्थापन {{math|{{mset| ''x'' ↦ ''h''(''a'',''y''), ''z'' ↦ ''b'' }}}} प्रयुक्त शब्द के लिए होता है.
+{|
-प्रथम-क्रम उदाहरण के रूप में प्रतिस्थापन लागू करना {{math|{{mset| ''x'' ↦ ''h''(''a'',''y''), ''z'' ↦ ''b'' }}}}शब्द के लिए होता है.
- {|
 |-
 |
@@ Line 33: / Line 29: @@
 | <math> ), y)</math>
 |-
-| yields &nbsp;
+| प्रतिफल
 |-
 |
@@ Line 44: / Line 40: @@
 ==='''सामान्यीकरण, विशेषज्ञता'''===
-यदि एक शब्द <math>t</math> एक पद के समतुल्य एक उदाहरण है <math>u</math>, अर्थात्, यदि <math>t\sigma \equiv u</math> कुछ प्रतिस्थापन के लिए <math>\sigma</math>, तब <math>t</math> से अधिक सामान्य कहा जाता है <math>u</math>, और <math>u</math> से अधिक विशेष कहा जाता है, या उसमें सम्मिलित किया जाता है, <math>t</math>. उदाहरण के लिए, <math>x\oplus a</math> से अधिक सामान्य है <math>a\oplus b</math> यदि ⊕ क्रमविनिमेय संपत्ति है, तब से <math>(x\oplus a) \{x\mapsto b\} = b\oplus a\equiv a\oplus b</math>.
+यदि एक शब्द <math>t</math> एक पद के समतुल्य एक उदाहरण है <math>u</math>, अर्थात्, यदि <math>t\sigma \equiv u</math> कुछ प्रतिस्थापन के लिए <math>\sigma</math>, तब <math>t</math> से अधिक सामान्य कहा जाता है <math>u</math>, और <math>u</math> से अधिक विशेष कहा जाता है या उसमें सम्मिलित किया जाता है, <math>t</math>. उदाहरण के लिए, <math>x\oplus a</math> से अधिक सामान्य है <math>a\oplus b</math> यदि ⊕ क्रमविनिमेय x, के रूप में है तब <math>(x\oplus a) \{x\mapsto b\} = b\oplus a\equiv a\oplus b</math>.गुणधर्म है
-यदि ≡ शब्दों की शाब्दिक वाक्यविन्यास के रूप में पहचान है, तो एक शब्द दूसरे की तुलना में अधिक सामान्य और अधिक विशेष दोनों हो सकते है, यदि दोनों शब्द मात्र उनके परिवर्तनीय नामों में भिन्न हों न कि उनकी सिंटैक्टिक संरचना में ऐसे शब्दों को परिवर्त या एक-दूसरे का नाम बदलना कहा जाता है।
+यदि ≡ शब्दों की शाब्दिक वाक्यविन्यास के रूप में पहचान है, तो एक शब्द दूसरे की तुलना में अधिक सामान्य और अधिक विशेष दोनों हो सकते है, यदि दोनों शब्द मात्र उनके परिवर्तनीय नामों में भिन्न हों न कि उनकी वाक्यात्मक संरचना में ऐसे शब्दों को परिवर्त या एक-दूसरे का नाम बदलना कहा जाता है।
 उदाहरण के लिए,
@@ Line 64: / Line 60: @@
 उदाहरण के लिए, यदि ⊕ [[निष्क्रिय]] है, अर्थात यदि सदैव <math>x \oplus x \equiv x</math>, फिर पद <math>x\oplus y</math> से अधिक सामान्य है <math>z</math>,<ref group="note">since <math>(x\oplus y) \{x\mapsto z, y \mapsto z\} = z\oplus z \equiv z</math></ref> और इसके विपरीत,<ref group="note">since {{math|1=''z'' {{mset|''z'' ↦ ''x'' ⊕ ''y''}} = ''x'' ⊕ ''y''}}</ref> यद्यपि <math>x\oplus y</math> और <math>z</math> भिन्न-भिन्न संरचना के हैं.
-एक प्रतिस्थापन <math>\sigma</math> प्रतिस्थापन से अधिक विशेष होता है या उसमें सम्मिलित होता है <math>\tau</math> यदि <math>t\sigma</math> द्वारा सम्मिलित किया गया है <math>t\tau</math> प्रत्येक पद के लिए <math>t</math>. हम भी यही कहते हैं <math>\tau</math> से अधिक सामान्य है <math>\sigma</math>. अधिक फॉर्मल रूप से, एक गैर-रिक्त अनंत सेट लें <math>V</math> सहायक चर जैसे कि को E समीकरण नहीं <math>l_i \doteq r_i</math> यूनिफिकेशन समस्या में चर के रूप में सम्मिलित हैं <math>V</math>. फिर एक प्रतिस्थापन <math>\sigma</math> किसी अन्य प्रतिस्थापन द्वारा सम्मिलित किया गया है <math>\tau</math> यदि कोई प्रतिस्थापन है <math>\theta</math> ऐसा कि सभी शर्तों के लिए <math>X\notin V</math>, <math>X\sigma \equiv X\tau\theta</math>.<ref name="Vukmirovic" />उदाहरण के लिए <math> \{x \mapsto a, y \mapsto a \}</math> द्वारा सम्मिलित किया गया है <math>\tau = \{x\mapsto y\}</math>, का उपयोग करना <math>\theta=\{y\mapsto a\}</math>, लेकिन
+एक प्रतिस्थापन <math>\sigma</math> प्रतिस्थापन से अधिक विशेष होता है या उसमें सम्मिलित होता है <math>\tau</math> यदि <math>t\sigma</math> द्वारा सम्मिलित किया गया है <math>t\tau</math> प्रत्येक पद के लिए <math>t</math>. हम भी यही कहते हैं <math>\tau</math> से अधिक सामान्य है <math>\sigma</math>. अधिक फॉर्मल रूप से एक गैर-रिक्त अनंत समुच्चय लें <math>V</math> सहायक चर जैसे कि को E समीकरण नहीं <math>l_i \doteq r_i</math> एकीकरण समस्या में चर के रूप में सम्मिलित हैं <math>V</math>. फिर एक प्रतिस्थापन <math>\sigma</math> किसी अन्य प्रतिस्थापन द्वारा सम्मिलित किया गया है <math>\tau</math> यदि कोई प्रतिस्थापन है <math>\theta</math> ऐसा कि सभी शर्तों के लिए <math>X\notin V</math>, <math>X\sigma \equiv X\tau\theta</math>.<ref name="Vukmirovic" />उदाहरण के लिए <math> \{x \mapsto a, y \mapsto a \}</math> द्वारा सम्मिलित किया गया है <math>\tau = \{x\mapsto y\}</math>, का उपयोग करना <math>\theta=\{y\mapsto a\}</math>, लेकिन
   <math>\sigma = \{x\mapsto a\}</math> में सम्मिलित नहीं है <math>\tau = \{x\mapsto y\}</math>, जैसा <math>f(x, y)\sigma = f(a, y)</math> का उदाहरण नहीं है
 <math>f(x, y) \tau = f(y, y)</math>.<ref>{{cite book |last1=Apt |first1=Krzysztof R. |title=लॉजिक प्रोग्रामिंग से लेकर प्रोलॉग तक|date=1997 |publisher=Prentice Hall |location=London Munich |isbn=013230368X |edition=1. publ |url=https://homepages.cwi.nl/~apt/book.ps|p=24}}</ref><nowiki>}} के रूप में होता है.</nowiki>
-==='''सलूशन सेट'''===
+==='''हल समुच्चय''' ===
-एक प्रतिस्थापन σ यूनिफिकेशन समस्या E के रूप में एक सलूशन है यदि {{math|''l''<sub>''i''</sub>σ ≡ ''r''<sub>''i''</sub>σ}} के लिए <math>i = 1, ..., n</math>. ऐसे प्रतिस्थापन को E का एकीकरण कर्ता भी कहा जाता है।
+एक प्रतिस्थापन σ एकीकरण समस्या E के रूप में एक हल है यदि {{math|''l''<sub>''i''</sub>σ ≡ ''r''<sub>''i''</sub>σ}} के लिए <math>i = 1, ..., n</math>. ऐसे प्रतिस्थापन को E का एकीकरण कर्ता भी कहा जाता है।
-उदाहरण के लिए, यदि ⊕ साहचर्य है, तो यूनिफिकेशन समस्या {''x'' ⊕ ''a'' ≐ ''a'' ⊕ ''x'' } के सलूशन हैं {''x'' ↦ ''a' '}, {''x'' ↦ ''a'' ⊕ ''a''}, {''x'' ↦ ''a'' ⊕ ''a'' ⊕ ''a''}, आदि ,जबकि समस्या { ''x'' ⊕ ''a'' ≐ ''a'' } का कोई सलूशन नहीं होता है।''
+उदाहरण के लिए, यदि ⊕ साहचर्य है, तो एकीकरण समस्या {''x'' ⊕ ''a'' ≐ ''a'' ⊕ ''x'' } के हल हैं {''x'' ↦ ''a' '}, {''x'' ↦ ''a'' ⊕ ''a''}, {''x'' ↦ ''a'' ⊕ ''a'' ⊕ ''a''}, आदि ,जबकि समस्या { ''x'' ⊕ ''a'' ≐ ''a'' } का कोई हल नहीं होता है।''
-दी गई यूनिफिकेशन समस्या E के लिए, एकीकरण कर्ताओं के एक सेट ''S'' को पूर्ण कहा जाता है यदि प्रत्येक सलूशन प्रतिस्थापन को ''एस'' में कुछ प्रतिस्थापन द्वारा समाहित किया जाता है। एक पूर्ण प्रतिस्थापन सेट निरंतर उपलब्ध होता है, उदाहरण के लिए सभी समाधानों का सेट लेकिन कुछ रूपरेखाओं में जैसे कि अप्रतिबंधित उच्च-क्रम यूनिफिकेशन में यह निर्धारित करने की समस्या  होती है कि क्या पूर्ण प्रतिस्थापन सेट गैर रिक्त अनिर्णीत रूप में होता है।
+दी गई एकीकरण समस्या E के लिए, एकीकरण कर्ताओं के एक समुच्चय ''S'' को पूर्ण कहा जाता है यदि प्रत्येक हल प्रतिस्थापन को ''एस'' में कुछ प्रतिस्थापन द्वारा समाहित किया जाता है। एक पूर्ण प्रतिस्थापन समुच्चय निरंतर उपलब्ध होता है, उदाहरण के लिए सभी समाधानों का समुच्चय लेकिन कुछ रूप रेखाओं में जैसे कि अप्रतिबंधित उच्च-क्रम एकीकरण में यह निर्धारित करने की समस्या होती है, कि क्या पूर्ण प्रतिस्थापन समुच्चय गैर रिक्त अनिर्णीत रूप में होता है।
-समुच्चय ''S'' को न्यूनतम कहा जाता है, इसका कोई भी सदस्य दूसरे को सम्मिलित नहीं करता है। इस प्रकार रूपरेखा के आधार पर एक पूर्ण और न्यूनतम प्रतिस्थापन सेट में शून्य एक, परिमित रूप से कई या अनंत रूप से कई सदस्य होते हैं या अनावश्यक सदस्यों की अनंत श्रृंखला के कारण पूर्ण रूप में उपलब्ध नहीं होते हैं।<ref>{{cite journal|first1=François|last1=Fages|first2=Gérard|last2=Huet|title=समीकरण सिद्धांतों में यूनिफायर और मैचर्स का पूरा सेट|journal=Theoretical Computer Science|volume=43|pages=189–200|year=1986|doi=10.1016/0304-3975(86)90175-1|doi-access=free}}</ref> इस प्रकार, सामान्यतः यूनिफिकेशन कलनविधि पूर्ण सेट के एक सीमित सन्निकटन की गणना करते हैं, जो न्यूनतम रूप में हो भी सकता है और नहीं भी हो सकता है, चूंकि अधिकांश कलनविधि जब संभव होता है तो निरर्थक एकीकरण कर्ताओं से बचते हैं।<ref name="Vukmirovic" /> प्रथम-क्रम सिंटैक्टिक यूनिफिकेशन के लिए, मार्टेली और मोंटानारी<ref name="Martelli.Montanari.1982">{{cite journal|first1=Alberto|last1=Martelli|first2=Ugo|last2=Montanari|title=एक कुशल एकीकरण एल्गोरिदम|journal=ACM Trans. Program. Lang. Syst.|volume=4|number=2|pages=258–282|date=Apr 1982|doi=10.1145/357162.357169|s2cid=10921306}}</ref> एक कलनविधि को दिया जाता है जो अघुलनशीलता की रिपोर्ट करता है या एकल यूनिफायर की गणना करता है, जो स्वयं एक पूर्ण और न्यूनतम प्रतिस्थापन सेट के रूप में बनाता है, जिसे सबसे सामान्य यूनिफायर कहा जाता है।
+समुच्चय ''S'' को न्यूनतम कहा जाता है, इसका कोई भी सदस्य दूसरे को सम्मिलित नहीं करता है। इस प्रकार रूपरेखा के आधार पर एक पूर्ण और न्यूनतम प्रतिस्थापन समुच्चय में शून्य एक परिमित रूप से कई या अनंत रूप से कई सदस्य होते हैं या अनावश्यक सदस्यों की अनंत श्रृंखला के कारण पूर्ण रूप में उपलब्ध नहीं होते हैं।<ref>{{cite journal|first1=François|last1=Fages|first2=Gérard|last2=Huet|title=समीकरण सिद्धांतों में यूनिफायर और मैचर्स का पूरा सेट|journal=Theoretical Computer Science|volume=43|pages=189–200|year=1986|doi=10.1016/0304-3975(86)90175-1|doi-access=free}}</ref> इस प्रकार सामान्यतः एकीकरण कलन विधि पूर्ण समुच्चय के एक सीमित सन्निकटन की गणना करते हैं, जो न्यूनतम रूप में हो भी सकता है और नहीं भी हो सकता है, चूंकि अधिकांश कलन विधि जब संभव होता है तो निरर्थक एकीकरण कर्ताओं से बचते हैं।<ref name="Vukmirovic" /> प्रथम-क्रम वाक्यात्मक एकीकरण के लिए, मार्टेली और मोंटानारी<ref name="Martelli.Montanari.1982">{{cite journal|first1=Alberto|last1=Martelli|first2=Ugo|last2=Montanari|title=एक कुशल एकीकरण एल्गोरिदम|journal=ACM Trans. Program. Lang. Syst.|volume=4|number=2|pages=258–282|date=Apr 1982|doi=10.1145/357162.357169|s2cid=10921306}}</ref> एक कलन विधि को दिया जाता है, जो अघुलनशीलता की रिपोर्ट करता है या एकल यूनिफायर की गणना करता है, जो स्वयं एक पूर्ण और न्यूनतम प्रतिस्थापन समुच्चय के रूप में बनाता है, जिसे सबसे सामान्य यूनिफायर कहा जाता है।
-=='''प्रथम-क्रम शब्दों का सिंटैक्टिक एकीकरण'''==
+=='''प्रथम-क्रम शब्दों का वाक्यात्मकएकीकरण'''==
-[[File:Triangle diagram of syntactic unification svg.svg|thumb|वाक्यविन्यास की दृष्टि से एकीकृत शब्दों का योजनाबद्ध त्रिभुज आरेख टी<sub>1</sub> और टी<sub>2</sub> एक प्रतिस्थापन द्वारा पी]]प्रथम-क्रम शब्दों का सिंटैक्टिक यूनिफिकेशन सबसे व्यापक रूप से उपयोग किया जाने वाला यूनिफिकेशन ढांचा है।
+[[File:Triangle diagram of syntactic unification svg.svg|thumb|प्रतिस्थापन σ द्वारा टर्म t1 और t2 को वाक्यात्मकरूप से एकीकृत करने का योजनाबद्ध त्रिभुज आरेख है]]प्रथम-क्रम शब्दों का वाक्यात्मक एकीकरण सबसे व्यापक रूप से उपयोग किया जाने वाला एकीकरण ढांचा है।
-यह प्रथम-क्रम के पदों के समुच्चय T के रूप में आधारित है, (चरों के कुछ दिए गए समुच्चय V, स्थिरांकों के C और F पर)<sub>''n''</sub> n-ary फलन प्रतीकों का और ≡ सिंटैक्टिक समानता पर आधारित है।
+यह प्रथम-क्रम के पदों के समुच्चय T के रूप में आधारित है, (चरों के कुछ दिए गए समुच्चय V, स्थिरांकों के C और F पर)<sub>''n''</sub> n-ary फलन प्रतीकों का और ≡ वाक्यात्मक समानता पर आधारित है।
-इस ढांचे में, प्रत्येक सलूशन योग्य यूनिफिकेशन समस्या {{math|{{mset|''l''<sub>1</sub> ≐ ''r''<sub>1</sub>, ..., ''l''<sub>''n''</sub> ≐ ''r''<sub>''n''</sub>}}}} के पास पूर्ण, और स्पष्ट रूप से न्यूनतम, [[सिंगलटन (गणित)|एकल (गणित)]] सलूशन सेट है {{math|1={{mset|''σ''}}}}.
+इस ढांचे में, प्रत्येक हल योग्य एकीकरण समस्या {{math|{{mset|''l''<sub>1</sub> ≐ ''r''<sub>1</sub>, ..., ''l''<sub>''n''</sub> ≐ ''r''<sub>''n''</sub>}}}} के पास पूर्ण, और स्पष्ट रूप से न्यूनतम, [[सिंगलटन (गणित)|एकल (गणित)]] हल समुच्चय है {{math|1={{mset|''σ''}}}}.
 इसके सदस्य {{mvar|σ}} को समस्या का सबसे सामान्य एकीकरणकर्ता (एमजीयू) का रूप कहा जाता है।
-जब एमजीयू लागू किया जाता है तो प्रत्येक संभावित समीकरण के बायीं और दायीं ओर के पद सिंटैक्टिक रूप से समतुल्य हो जाते हैं। {{math|1=''l''<sub>1</sub>''σ'' = ''r''<sub>1</sub>''σ'' ∧ ... ∧ ''l''<sub>''n''</sub>''σ'' = ''r''<sub>''n''</sub>''σ''}}.
+जब एमजीयू प्रयुक्त किया जाता है तो प्रत्येक संभावित समीकरण के बायीं और दायीं ओर के पद वाक्यात्मक रूप से समतुल्य हो जाते हैं। {{math|1=''l''<sub>1</sub>''σ'' = ''r''<sub>1</sub>''σ'' ∧ ... ∧ ''l''<sub>''n''</sub>''σ'' = ''r''<sub>''n''</sub>''σ''}}.
 समस्या का कोई भी एकीकरणकर्ता समाहित हो जाता है<ref group="note">formally: each unifier τ satisfies {{math|1=∀''x'': ''xτ'' = (''xσ'')''ρ''}} for some substitution ρ</ref> एमजीयू द्वारा {{mvar|σ}}.
-एमजीयू वेरिएंट तक अद्वितीय है: यदि एस<sub>1</sub> और एस<sub>2</sub> दोनों एक ही सिंटैक्टिक यूनिफिकेशन समस्या के पूर्ण और न्यूनतम सलूशन सेट हैं, तो ''S''<sub>1</sub> = { ''σ''<sub>1</sub> } और ''S''<sub>2</sub> = { ''σ''<sub>2</sub> } कुछ प्रतिस्थापनों के लिए {{math|1=''σ''<sub>1</sub>}} और {{math|1=''σ''<sub>2</sub>,}} और {{math|1=''xσ''<sub>1</sub>}} का एक प्रकार है {{math|1=''xσ''<sub>2</sub>}} समस्या में आने वाले प्रत्येक चर x के लिए।
+एमजीयू वेरिएंट तक अद्वितीय है: यदि एस<sub>1</sub> और एस<sub>2</sub> दोनों एक ही वाक्यात्मक एकीकरण समस्या के पूर्ण और न्यूनतम हल समुच्चय हैं, तो ''S''<sub>1</sub> = { ''σ''<sub>1</sub> } और ''S''<sub>2</sub> = { ''σ''<sub>2</sub> } कुछ प्रतिस्थापनों के लिए {{math|1=''σ''<sub>1</sub>}} और {{math|1=''σ''<sub>2</sub>,}} और {{math|1=''xσ''<sub>1</sub>}} का एक प्रकार है {{math|1=''xσ''<sub>2</sub>}} समस्या में आने वाले प्रत्येक चर x के लिए है।
-उदाहरण के लिए, यूनिफिकेशन समस्या { x ≐ z, y ≐ f(x) } में एक एकीकृतकर्ता है { x ↦ z, y ↦ f(z) }, क्योंकि
+उदाहरण के लिए, एकीकरण समस्या { x ≐ z, y ≐ f(x) } में एक एकीकृतकर्ता है { x ↦ z, y ↦ f(z) }, क्योंकि
 :{|
 |-
@@ Line 115: / Line 111: @@
 यह सबसे सामान्य एकीकरणकर्ता के रूप में है
-समान समस्या के लिए अन्य एकीकरणकर्ता हैं, उदा. { x ↦ f(x<sub>1</sub>), y ↦ f(f(x<sub>1</sub>)), z ↦ f(x<sub>1</sub>) }, { x ↦ f(f(x<sub>1</sub>)), y ↦ f(f(f(x<sub>1</sub>))), z ↦ f(f(x<sub>1</sub>)) }, और इसी प्रकार ऐसे अपरिमित रूप से अनेक एकीकरणकर्ता के रूप में हैं।
+समान समस्या के लिए अन्य एकीकरणकर्ता हैं, उदा. { x ↦ f(x<sub>1</sub>), y ↦ f(f(x<sub>1</sub>)), z ↦ f(x<sub>1</sub>) }, { x ↦ f(f(x<sub>1</sub>)), y ↦ f(f(f(x<sub>1</sub>))), z ↦ f(f(x<sub>1</sub>)) }, और इसी प्रकार ऐसे अपरिमित रूप से अनेक एकीकरण कर्ता के रूप में हैं।
-एक अन्य उदाहरण के रूप में, समस्या g(x,x) ≐ f(y) का शाब्दिक पहचान होने के संबंध में कोई सलूशन नहीं है, क्योंकि बाएं और दाएं तरफ लागू कोई भी प्रतिस्थापन क्रमशः सबसे बाहरी g और f को बनाए रखेगा, और विभिन्न बाहरीतम फलन प्रतीकों वाले शब्द सिंटैक्टिक रूप से भिन्न होते हैं।
+एक अन्य उदाहरण के रूप में समस्या g(x,x) ≐ f(y) का शाब्दिक पहचान होने के संबंध में कोई हल नहीं है, क्योंकि बाएं और दाएं तरफ प्रयुक्त कोई भी प्रतिस्थापन क्रमशः सबसे बाहरी g और f को बनाए रखेगा, और विभिन्न बाहरीतम फलन प्रतीकों वाले शब्द वाक्यात्मक रूप से भिन्न होते हैं।
-==='''एक यूनिफिकेशन एल्गोरिथ्म'''===
+==='''एक एकीकरण कलन विधि''' ===
 {{Quote box|title=Robinson's 1965 unification algorithm
 |quote={{hidden begin}}
@@ Line 147: / Line 143: @@
 {{hidden end}}
 }}
-रॉबिन्सन (1965) द्वारा दिया गया पहला कलनविधि अधिक अप्रभावी था; cf डिब्बा।
+रॉबिन्सन (1965) द्वारा दिया गया पहला कलन विधि अधिक अप्रभावी था; cf डिब्बा।
-निम्नलिखित तेज़ कलनविधि की उत्पत्ति मार्टेली, मोंटानारी (1982) के रूप में हुई थी।<ref group="note">Alg.1, p.261. Their rule '''(a)''' corresponds to rule '''swap''' here, '''(b)''' to '''delete''', '''(c)''' to both '''decompose''' and '''conflict''', and '''(d)''' to both '''eliminate''' and '''check'''.</ref>
+निम्नलिखित तेज़ कलन विधि की उत्पत्ति मार्टेली, मोंटानारी (1982) के रूप में हुई थी।<ref group="note">Alg.1, p.261. Their rule '''(a)''' corresponds to rule '''swap''' here, '''(b)''' to '''delete''', '''(c)''' to both '''decompose''' and '''conflict''', and '''(d)''' to both '''eliminate''' and '''check'''.</ref>
-यह पेपर एक कुशल सिंटैक्टिक यूनिफिकेशन कलनविधि खोजने के पिछले प्रयासों को भी सूचीबद्ध करता है,<ref>{{cite report | author=Lewis Denver Baxter | title=एक व्यावहारिक रूप से रैखिक एकीकरण एल्गोरिदम| publisher=Univ. of Waterloo, Ontario | type=Res. Report | volume=CS-76-13 | url=https://cs.uwaterloo.ca/research/tr/1976/CS-76-13.pdf |date=Feb 1976 }}</ref><ref>{{cite thesis | author=Gérard Huet | title=Resolution d'Equations dans des Langages d'Ordre 1,2,...ω | publisher=Universite de Paris VII | type=These d'etat |date=Sep 1976 | author-link=Gérard Huet }}</ref><ref name="Martelli.Montanari.1976">{{cite report | author1=Alberto Martelli | author2=Ugo Montanari | name-list-style=amp | title=Unification in linear time and space: A structured presentation | publisher=Consiglio Nazionale delle Ricerche, Pisa | type=Internal Note | volume=IEI-B76-16 | url=http://puma.isti.cnr.it/publichtml/section_cnr_iei/cnr_iei_1976-B4-041.html | archive-url=https://web.archive.org/web/20150115070153/http://puma.isti.cnr.it/publichtml/section_cnr_iei/cnr_iei_1976-B4-041.html | url-status=dead | archive-date=2015-01-15 | date=Jul 1976 }}</ref><ref name="Paterson.Wegman.1978">{{cite journal | author=[[Michael Stewart Paterson]] and M.N. Wegman | title=रैखिक एकीकरण| journal=J. Comput. Syst. Sci. | volume=16 | number=2 | pages=158–167 |date=Apr 1978 | doi = 10.1016/0022-0000(78)90043-0 | doi-access=free }}</ref><ref>{{cite book | author=J.A. Robinson | chapter=Fast unification | editor=[[Woodrow W. Bledsoe]], Michael M. Richter | title=प्रोक. प्रमेय सिद्ध करने की कार्यशाला ओबेरवुल्फ़च| series=Oberwolfach Workshop Report | volume=1976/3 | chapter-url=http://oda.mfo.de/bsz325106819.html | date=Jan 1976 | author-link=J.A. Robinson }}{{Dead link|date=March 2021 |bot=InternetArchiveBot |fix-attempted=yes }}</ref><ref>{{cite journal | author=M. Venturini-Zilli | title=प्रथम-क्रम अभिव्यक्तियों के लिए एकीकरण एल्गोरिथ्म की जटिलता|journal= Calcolo | volume=12 |number=4 |pages= 361–372 |date= Oct 1975 | doi=10.1007/BF02575754| s2cid=189789152 }}</ref> और बताता है, कि रैखिक-समय कलनविधि की खोज मार्टेली, मोंटानारी (1976) द्वारा स्वतंत्र रूप से की गई थी।<ref name="Martelli.Montanari.1976" />और पैटरसन, वेगमैन (1976,<ref>{{cite conference | doi=10.1145/800113.803646 | url= | first1=M.S. |last1=Paterson |first2= M.N. |last2= Wegman | title=रैखिक एकीकरण| editor1-first=Ashok K. |editor1-last=Chandra |editor2-first= Detlef |editor2-last= Wotschke  |editor3-first= Emily P. |editor3-last=Friedman  |editor4-first= Michael A.|editor4-last= Harrison  | conference=Proceedings of the eighth annual ACM [[Symposium on Theory of Computing]] (STOC) | publisher=ACM | pages=181&ndash;186 | date=May 1976 }}</ref> 1978<ref name="Paterson.Wegman.1978" />).{{refn|Independent discovery is stated in Martelli, Montanari (1982),<ref name="Martelli.Montanari.1982"/> sect.1, p.259. Paterson's and Wegman's journal paper<ref name="Paterson.Wegman.1978"/> is dated 1978; however, the journal publisher received it in Sep.1976.|group=note}} का रूप होता है.
+यह पेपर एक कुशल वाक्यात्मक एकीकरण कलन विधि खोजने के पिछले प्रयासों को भी सूचीबद्ध करता है,<ref>{{cite report | author=Lewis Denver Baxter | title=एक व्यावहारिक रूप से रैखिक एकीकरण एल्गोरिदम| publisher=Univ. of Waterloo, Ontario | type=Res. Report | volume=CS-76-13 | url=https://cs.uwaterloo.ca/research/tr/1976/CS-76-13.pdf |date=Feb 1976 }}</ref><ref>{{cite thesis | author=Gérard Huet | title=Resolution d'Equations dans des Langages d'Ordre 1,2,...ω | publisher=Universite de Paris VII | type=These d'etat |date=Sep 1976 | author-link=Gérard Huet }}</ref><ref name="Martelli.Montanari.1976">{{cite report | author1=Alberto Martelli | author2=Ugo Montanari | name-list-style=amp | title=Unification in linear time and space: A structured presentation | publisher=Consiglio Nazionale delle Ricerche, Pisa | type=Internal Note | volume=IEI-B76-16 | url=http://puma.isti.cnr.it/publichtml/section_cnr_iei/cnr_iei_1976-B4-041.html | archive-url=https://web.archive.org/web/20150115070153/http://puma.isti.cnr.it/publichtml/section_cnr_iei/cnr_iei_1976-B4-041.html | url-status=dead | archive-date=2015-01-15 | date=Jul 1976 }}</ref><ref name="Paterson.Wegman.1978">{{cite journal | author=[[Michael Stewart Paterson]] and M.N. Wegman | title=रैखिक एकीकरण| journal=J. Comput. Syst. Sci. | volume=16 | number=2 | pages=158–167 |date=Apr 1978 | doi = 10.1016/0022-0000(78)90043-0 | doi-access=free }}</ref><ref>{{cite book | author=J.A. Robinson | chapter=Fast unification | editor=[[Woodrow W. Bledsoe]], Michael M. Richter | title=प्रोक. प्रमेय सिद्ध करने की कार्यशाला ओबेरवुल्फ़च| series=Oberwolfach Workshop Report | volume=1976/3 | chapter-url=http://oda.mfo.de/bsz325106819.html | date=Jan 1976 | author-link=J.A. Robinson }}{{Dead link|date=March 2021 |bot=InternetArchiveBot |fix-attempted=yes }}</ref><ref>{{cite journal | author=M. Venturini-Zilli | title=प्रथम-क्रम अभिव्यक्तियों के लिए एकीकरण एल्गोरिथ्म की जटिलता|journal= Calcolo | volume=12 |number=4 |pages= 361–372 |date= Oct 1975 | doi=10.1007/BF02575754| s2cid=189789152 }}</ref> और बताता है, कि रैखिक-समय कलन विधि की खोज मार्टेली, मोंटानारी (1976) द्वारा स्वतंत्र रूप से की गई थी।<ref name="Martelli.Montanari.1976" />और पैटरसन, वेगमैन (1976,<ref>{{cite conference | doi=10.1145/800113.803646 | url= | first1=M.S. |last1=Paterson |first2= M.N. |last2= Wegman | title=रैखिक एकीकरण| editor1-first=Ashok K. |editor1-last=Chandra |editor2-first= Detlef |editor2-last= Wotschke  |editor3-first= Emily P. |editor3-last=Friedman  |editor4-first= Michael A.|editor4-last= Harrison  | conference=Proceedings of the eighth annual ACM [[Symposium on Theory of Computing]] (STOC) | publisher=ACM | pages=181&ndash;186 | date=May 1976 }}</ref> 1978<ref name="Paterson.Wegman.1978" />).{{refn|Independent discovery is stated in Martelli, Montanari (1982),<ref name="Martelli.Montanari.1982"/> sect.1, p.259. Paterson's and Wegman's journal paper<ref name="Paterson.Wegman.1978"/> is dated 1978; however, the journal publisher received it in Sep.1976.|group=note}} का रूप होता है.
 एक परिमित समुच्चय दिया गया है <math>G = \{ s_1 \doteq t_1, ..., s_n \doteq t_n \}</math> संभावित समीकरणों का रूप होता है. ,
-कलनविधि इसे फॉर्म के समीकरणों के समतुल्य सेट में बदलने के लिए नियम लागू करता है
+कलन विधि इसे फॉर्म के समीकरणों के समतुल्य समुच्चय में बदलने के लिए नियम प्रयुक्त करता है.
 { ''x''<sub>1</sub> ≐ ''u''<sub>1</sub>, ..., ''x<sub>m</sub>'' ≐ ''u<sub>m</sub>'' }
-कहां x<sub>1</sub>, ..., x<sub>''m''</sub> भिन्न-भिन्न चर हैं और''u''<sub>1</sub>, ..., ''u<sub>m</sub>'' ऐसे पद हैं जिनमें x में से कोई भी नहीं है<sub>''i''</sub>.
+जहाँ x<sub>1</sub>, ..., x<sub>''m''</sub> भिन्न-भिन्न चर हैं और''u''<sub>1</sub>, ..., ''u<sub>m</sub>'' ऐसे पद हैं जिनमें x में से कोई भी नहीं है<sub>''i''</sub>.
-इस फॉर्म के एक सेट को प्रतिस्थापन के रूप में पढ़ा जा सकता है।
+इस फॉर्म के एक समुच्चय को प्रतिस्थापन के रूप में पढ़ा जा सकता है।
-यदि कोई सलूशन नहीं है तो कलनविधि ⊥ के साथ समाप्त हो जाता है; अन्य लेखक Ω , {} के रूप में उपयोग करते हैं या उस स्थिति में विफल हो जाते हैं।
+यदि कोई हल नहीं है, तो कलन विधि ⊥ के साथ समाप्त हो जाता है; अन्य लेखक Ω , {} के रूप में उपयोग करते हैं या उस स्थिति में विफल हो जाते हैं।
 समस्या G में चर x की सभी घटनाओं को पद t से प्रतिस्थापित करने की क्रिया को G {x ↦ t} दर्शाया गया है।
@@ Line 208: / Line 204: @@
-===='''चेक होता है'''====
+===='''ओक्कुर चेक''' ====
-{{main|Occurs check}}
+{{main|ओक्कुर चेक}}
-एक चर x को एक ऐसे पद के साथ एकीकृत करने का प्रयास जिसमें x एक सख्त उपपद x ≐ f(..., x, ...) के रूप में हो, x के सलूशन के रूप में एक अनंत पद की ओर ले जाता है, क्योंकि x स्वयं के एक उपपद के रूप में घटित होता है.
+एक चर x को एक ऐसे पद के साथ एकीकृत करने का प्रयास जिसमें x एक सख्त उपपद x ≐ f(..., x, ...) के रूप में हो, x के हल के रूप में एक अनंत पद की ओर ले जाता है, क्योंकि x स्वयं के एक उपपद के रूप में घटित होता है
-जैसा कि ऊपर परिभाषित किया गया है (परिमित) प्रथम-क्रम शब्दों के सेट में समीकरण x ≐ f(..., x, ...) का कोई सलूशन नहीं है; इसलिए उन्मूलन नियम मात्र तभी लागू किया जा सकता है यदि x ∉ वार्स(t)।
+जैसा कि ऊपर परिभाषित किया गया है (परिमित) प्रथम-क्रम शब्दों के समुच्चय में समीकरण x ≐ f(..., x, ...) का कोई हल नहीं है; इसलिए उन्मूलन नियम मात्र तभी प्रयुक्त किया जा सकता है यदि x ∉ वार्स(t)।
-चूँकि वह अतिरिक्त जाँच जिसे 'एक्सेस चेक' कहा जाता है, कलनविधि को धीमा कर देती है, इसलिए इसे छोड़ दिया जाता है, उदाहरण के लिए अधिकांश प्रोलॉग सिस्टम में होता है।
+चूँकि वह अतिरिक्त जाँच जिसे 'एक्सेस चेक' कहा जाता है, कलन विधि को धीमा कर देती है, इसलिए इसे छोड़ दिया जाता है, उदाहरण के लिए अधिकांश प्रोलॉग प्रणाली में होता है।
-सैद्धांतिक दृष्टिकोण से, चेक को छोड़ना अनंत पेड़ों पर समीकरणों को हल करने के समतुल्य है, नीचे अनंत पदों का #यूनिफिकेशन के रूप में देख़ते है।
+सैद्धांतिक दृष्टिकोण से, चेक को छोड़ना अनंत पेड़ों पर समीकरणों को हल करने के समतुल्य है, नीचे अनंत पदों का # एकीकरण के रूप में देख़ते है।
 ===='''समाप्ति का प्रमाण'''====
-कलनविधि की समाप्ति के प्रमाण के लिए ट्रिपल पर विचार करें <math>\langle n_{var}, n_{lhs}, n_{eqn}\rangle</math>
+कलन विधि की समाप्ति के प्रमाण के लिए ट्रिपल पर विचार करें <math>\langle n_{var}, n_{lhs}, n_{eqn}\rangle</math>
-जहाँ {{math|''n''<sub>''var''</sub>}} समीकरण सेट में एक से अधिक बार आने वाले चरों की संख्या है, {{math|''n''<sub>''lhs''</sub>}} फलन प्रतीकों और स्थिरांकों की संख्या होती है'
+जहाँ {{math|''n''<sub>''var''</sub>}} समीकरण समुच्चय में एक से अधिक बार आने वाले चरों की संख्या है, {{math|''n''<sub>''lhs''</sub>}} फलन प्रतीकों और स्थिरांकों की संख्या होती है'
 संभावित समीकरणों के बाईं ओर और {{math|''n''<sub>''eqn''</sub>}} समीकरणों की संख्या के रूप में है.
-जब नियम उन्मूलन लागू किया जाता है, {{math|''n''<sub>''var''</sub>}} घट जाती है, क्योंकि G से x हटा दिया जाता है और मात्र { x ≐ t } में रखा जाता है।
+जब नियम उन्मूलन प्रयुक्त किया जाता है, {{math|''n''<sub>''var''</sub>}} घट जाती है, क्योंकि G से x हटा दिया जाता है और मात्र { x ≐ t } में रखा जाता है।
-कोई अन्य नियम लागू करने से कभी वृद्धि नहीं हो सकती {{math|''n''<sub>''var''</sub>}} दोबारा होता है ।
+कोई अन्य नियम प्रयुक्त करने से कभी वृद्धि नहीं हो सकती {{math|''n''<sub>''var''</sub>}} दोबारा होता है ।
-जब नियम विघटित, संघर्ष, या अदला-बदली लागू के रूप में किया जाता है, {{math|''n''<sub>''lhs''</sub>}} कम हो जाता है, क्योंकि कम से कम बायीं ओर का सबसे बाहरी f गायब हो जाता है।
+जब नियम विघटित, संघर्ष, या अदला-बदली प्रयुक्त के रूप में किया जाता है, {{math|''n''<sub>''lhs''</sub>}} कम हो जाता है, क्योंकि कम से कम बायीं ओर का सबसे बाहरी f गायब हो जाता है।
-बाकी किसी भी नियम को लागू करने से डिलीट या चेक नहीं बढ़ सकेगा {{math|''n''<sub>''lhs''</sub>}}, लेकिन घट जाती है {{math|''n''<sub>''eqn''</sub>}}.
+बाकी किसी भी नियम को प्रयुक्त करने से डिलीट या चेक नहीं बढ़ सकेगा {{math|''n''<sub>''lhs''</sub>}}, लेकिन घट जाती है {{math|''n''<sub>''eqn''</sub>}}.
-इसलिए किसी भी नियम को लागू करने से तीन गुना कम हो जाता है <math>\langle n_{var}, n_{lhs}, n_{eqn}\rangle</math> [[शब्दकोषीय क्रम]] के संबंध में जो मात्र सीमित संख्या में ही संभव है।
+इसलिए किसी भी नियम को प्रयुक्त करने से तीन गुना कम हो जाता है <math>\langle n_{var}, n_{lhs}, n_{eqn}\rangle</math> [[शब्दकोषीय क्रम]] के संबंध में जो मात्र सीमित संख्या में ही संभव है।
-[[कॉनर मैकब्राइड]] देखते हैं<ref>{{cite journal|last=McBride|first=Conor|title=संरचनात्मक प्रत्यावर्तन द्वारा प्रथम-क्रम एकीकरण|journal=Journal of Functional Programming|date=October 2003|volume=13|issue=6|pages=1061–1076|doi=10.1017/S0956796803004957|url=http://strictlypositive.org/unify.ps.gz|access-date=30 March 2012|issn=0956-7968|citeseerx=10.1.1.25.1516|s2cid=43523380 }}</ref> [[एपिग्राम (प्रोग्रामिंग भाषा)|एपिग्राम (प्रोग्रामिंग लैंग्वेज)]] जैसी आश्रित रूप से टाइप की गई लैंग्वेज में यूनिफिकेशन जिस संरचना का उपयोग करता है, उसे व्यक्त करके रॉबिन्सन के यूनिफिकेशन कलनविधि को चर की संख्या पर पुनरावर्ती बनाया जा सकता है, जिस स्थिति में एक भिन्न समाप्ति प्रमाण अनावश्यक हो जाता है।
+[[कॉनर मैकब्राइड]] देखते हैं<ref>{{cite journal|last=McBride|first=Conor|title=संरचनात्मक प्रत्यावर्तन द्वारा प्रथम-क्रम एकीकरण|journal=Journal of Functional Programming|date=October 2003|volume=13|issue=6|pages=1061–1076|doi=10.1017/S0956796803004957|url=http://strictlypositive.org/unify.ps.gz|access-date=30 March 2012|issn=0956-7968|citeseerx=10.1.1.25.1516|s2cid=43523380 }}</ref> [[एपिग्राम (प्रोग्रामिंग भाषा)|एपिग्राम (प्रोग्रामिंग लैंग्वेज)]] जैसी आश्रित रूप से टाइप की गई लैंग्वेज में एकीकरण जिस संरचना का उपयोग करता है, उसे व्यक्त करके रॉबिन्सन के एकीकरण कलन विधि को चर की संख्या पर पुनरावर्ती बनाया जा सकता है, जिस स्थिति में एक भिन्न समाप्ति प्रमाण अनावश्यक हो जाता है।
-==='''प्रथम-क्रम शब्दों के सिंटैक्टिक यूनिफिकेशन के उदाहरण'''===
+==='''प्रथम-क्रम शब्दों के वाक्यात्मकएकीकरण के उदाहरण'''===
 प्रोलॉग सिंटैक्टिकल कन्वेंशन में अपर केस अक्षर से प्रारंभ होने वाला प्रतीक एक परिवर्तनीय नाम है; एक प्रतीक जो छोटे अक्षर से प्रारंभ होता है. वह एक फलन प्रतीक है, अल्पविराम का उपयोग तार्किक और ऑपरेटर के रूप में किया जाता है।
@@ Line 245: / Line 242: @@
 ! प्रकल संकेतन !! गणितीय संकेतन !! एकताकारी प्रतिस्थापन !! निरूपण
 |-
-| <code> a = a </code> || { ''a'' = ''a'' } ||  {}  || सफल होता है. (टॉटोलॉजी)
+| <code> a = a </code> || { ''a'' = ''a'' } ||  {}  || सक्सीड (टॉटोलॉजी)
 |-
 | <code> a = b </code> || { ''a'' = ''b'' }  || ⊥ || a और b मेल नहीं खाते
 |-
-| <code> X = X </code> || { ''x'' = ''x'' } || {} || सफल होता है. (टॉटोलॉजी)
+| <code> X = X </code> || { ''x'' = ''x'' } || {} || सक्सीड (टॉटोलॉजी)
 |-
 | <code> a = X </code> || { ''a'' = ''x'' }  || { ''x'' ↦ ''a'' } || ''x'' स्थिरांक के साथ एकीकृत है ''a''
 |-
-| <code> X = Y </code> || { ''x'' = ''y'' }  || { ''x'' ↦ ''y'' } || x और y उपनाम हैं
+| <code> X = Y </code> || { ''x'' = ''y'' }  || { ''x'' ↦ ''y'' } || x और y अलियास हैं
 |-
 | <code> f(a,X) = f(a,b) </code> || { ''f''(''a'',''x'') = ''f''(''a'',''b'') } ||  { ''x'' ↦ ''b'' } || फलन और स्थिरांक प्रतीक मेल खाते हैं, x स्थिरांक b के साथ एकीकृत है
@@ Line 259: / Line 256: @@
 | <code> f(a) = g(a) </code> || { ''f''(''a'') = ''g''(''a'') }  || ⊥ || <code>f</code>और<code>g</code>मेल नहीं खाते
 |-
-| <code> f(X) = f(Y) </code> || { ''f''(''x'') = ''f''(''y'') } || { ''x'' ↦ ''y'' } || x और y उपनाम हैं
+| <code> f(X) = f(Y) </code> || { ''f''(''x'') = ''f''(''y'') } || { ''x'' ↦ ''y'' } || x और y अलियास हैं
 |-
 | <code> f(X) = g(Y) </code> || { ''f''(''x'') = ''g''(''y'') } || ⊥ || <code>f</code>और<code>g</code>मेल नहीं खाते
 |-
-| <code> f(X) = f(Y,Z) </code> || { ''f''(''x'') = ''f''(''y'',''z'') } || ⊥ || विफल रहता है.<code>f</code> फलन प्रतीकों में अलग-अलग योग्यताएं होती हैं
+| <code> f(X) = f(Y,Z) </code> || { ''f''(''x'') = ''f''(''y'',''z'') } || ⊥ || फाल्स <code>f</code> फलन प्रतीकों में भिन्न -भिन्न योग्यताएं होती हैं
 |-
 | <code> f(g(X)) = f(Y) </code> || { ''f''(''g''(''x'')) = ''f''(''y'') } || { ''y'' ↦ ''g''(''x'') } || y को पद के साथ एकीकृत करता है {{tmath|g(x)}}
@@ Line 269: / Line 266: @@
 | <code> f(g(X),X) = f(Y,a) </code> || { ''f''(''g''(''x''),''x'') = ''f''(''y'',''a'') } || { ''x'' ↦ ''a'', ''y'' ↦ ''g''(''a'') } || x को स्थिरांक a के साथ और y को पद के साथ एकीकृत करता है {{tmath|g(a)}}
 |-
-| <code> X = f(X) </code> || { ''x'' = ''f''(''x'') } || should be ⊥ || प्रथम-क्रम लॉजिक और कई आधुनिक प्रोलॉग बोलियों में रिटर्न ⊥ (होता है [[चेक द्वारा लागू]])।
+| <code> X = f(X) </code> || { ''x'' = ''f''(''x'') } || should be ⊥ || प्रथम-क्रम लॉजिक और कई आधुनिक प्रोलॉग बोलियों में रिटर्न ⊥ ओक्कुर चेक [[चेक द्वारा लागू|द्वारा प्रयुक्त]] होता है।
 पारंपरिक प्रोलॉग और प्रोलॉग II में<code>x</code>को अनंत पद के साथ एकीकृत करने में सफलता मिलती है<code>x=f(f(f(f(...))))</code>.
 |-
 | <code> X = Y, Y = a </code> || { ''x'' = ''y'', ''y'' = ''a'' } || { ''x'' ↦ ''a'', ''y'' ↦ ''a'' } || x और y दोनों स्थिरांक a के साथ एकीकृत हैं
 |-
-| <code> a = Y, X = Y </code> || { ''a'' = ''y'', ''x'' = ''y'' } || { ''x'' ↦ ''a'', ''y'' ↦ ''a'' } || जैसा कि ऊपर बताया गया है (सेट में समीकरणों का क्रम मायने नहीं रखता)
+| <code> a = Y, X = Y </code> || { ''a'' = ''y'', ''x'' = ''y'' } || { ''x'' ↦ ''a'', ''y'' ↦ ''a'' } || जैसा कि ऊपर बताया गया है (समुच्चय में समीकरणों का क्रम मायने नहीं रखता हैं)
 |-
-| <code> X = a, b = X </code> || { ''x'' = ''a'', ''b'' = ''x'' }  || ⊥ || विफल रहता है. a और b मेल नहीं खाते हैं, इसलिए X को दोनों के साथ एकीकृत नहीं किया जा सकता है
+| <code> X = a, b = X </code> || { ''x'' = ''a'', ''b'' = ''x'' }  || ⊥ || फाल्स a और b मेल नहीं खाते हैं, इसलिए X को दोनों के साथ एकीकृत नहीं किया जा सकता है
 |}
-[[File:Unification exponential blow-up svg.svg|thumb|अपने कम से कम सामान्य उदाहरण के लिए तेजी से बड़े पेड़ वाले दो शब्द। इसका निर्देशित चक्रीय आलेख प्रतिनिधित्व (सबसे दाहिना, नारंगी भाग) अभी भी रैखिक बनावट का है।]]टर्म (लॉजिक )#शब्दों के साथ संचालन की सिंटैक्टिक प्रथम-क्रम यूनिफिकेशन समस्या का सबसे सामान्य एकीकरणकर्ता {{mvar|n}} के रूप में बनावट हो सकता है {{math|2<sup>''n''</sup>}}. उदाहरण के लिए समस्या {{tmath| (((a*z)*y)*x)*w \doteq w*(x*(y*(z*a))) }} में सबसे सामान्य एकीकरणकर्ता है' {{tmath| \{ z \mapsto a,  y \mapsto a*a,  x \mapsto (a*a)*(a*a),  w \mapsto ((a*a)*(a*a))*((a*a)*(a*a)) \} }}, सीf. चित्र। इस प्रकार के विस्फोट के कारण होने वाली घातीय समय जटिलता से बचने के लिए उन्नत यूनिफिकेशन कलनविधि पेड़ों के अतिरिक्त निर्देशित एसाइक्लिक आलेख़ (डैग) पर काम करते हैं।{{refn|e.g. Paterson, Wegman (1978),<ref name="Paterson.Wegman.1978"/> sect.2, p.159}}
+[[File:Unification exponential blow-up svg.svg|thumb|अपने कम से कम सामान्य उदाहरण के लिए तेजी से बड़े पेड़ वाले दो शब्द। इसका निर्देशित चक्रीय आलेख प्रतिनिधित्व (सबसे दाहिना, नारंगी भाग) अभी भी रैखिक बनावट का है।]]टर्म (लॉजिक )#शब्दों के साथ संचालन की वाक्यात्मक प्रथम क्रम एकीकरण समस्या का सबसे सामान्य एकीकरणकर्ता {{mvar|n}} के रूप में बनावट हो सकता है {{math|2<sup>''n''</sup>}}. उदाहरण के लिए समस्या {{tmath| (((a*z)*y)*x)*w \doteq w*(x*(y*(z*a))) }} में सबसे सामान्य एकीकरणकर्ता है' {{tmath| \{ z \mapsto a,  y \mapsto a*a,  x \mapsto (a*a)*(a*a),  w \mapsto ((a*a)*(a*a))*((a*a)*(a*a)) \} }}, सीf. चित्र। इस प्रकार के विस्फोट के कारण होने वाली घातीय समय जटिलता से बचने के लिए उन्नत एकीकरण कलन विधि पेड़ों के अतिरिक्त निर्देशित एसाइक्लिक आलेख़ (डैग) पर काम करते हैं।{{refn|e.g. Paterson, Wegman (1978),<ref name="Paterson.Wegman.1978"/> sect.2, p.159}}
 ==='''अनुप्रयोग: लॉजिक प्रोग्रामिंग में एकीकरण'''===
-यूनिफिकेशन की अवधारणा लॉजिक प्रोग्रामिंग के पीछे मुख्य विचारों में से एक है, जिसे [[प्रोलॉग]] लैंग्वेज के माध्यम से जाना जाता है। यह चर की सामग्री को बांधने के तंत्र का प्रतिनिधित्व करता है और इसे एक प्रकार के एक बार के असाइनमेंट के रूप में देखा जा सकता है। प्रोलॉग में इस ऑपरेशन को समानता प्रतीक द्वारा दर्शाया जाता है <code>=</code> लेकिन चर को इंस्टेंटिएट करते समय भी किया जाता है (नीचे देखें)। समानता चिन्ह के प्रयोग से इसका प्रयोग अन्य लैंग्वेज में भी किया जाता है <code>=</code>अपितु कई ऑपरेशनों के संयोजन में भी सम्मिलित होता है <code>+</code>, <code>-</code>, <code>*</code>, <code>/</code>. प्रकार अनुमान कलनविधि सामान्यतः यूनिफिकेशन पर आधारित होते हैं।
+एकीकरण की अवधारणा लॉजिक प्रोग्रामिंग के पीछे मुख्य विचारों में से एक है, जिसे [[प्रोलॉग]] लैंग्वेज के माध्यम से जाना जाता है। यह चर की सामग्री को बांधने के तंत्र का प्रतिनिधित्व करता है और इसे एक प्रकार के एक बार के असाइनमेंट के रूप में देखा जा सकता है। प्रोलॉग में इस ऑपरेशन को समानता प्रतीक द्वारा दर्शाया जाता है <code>=</code> लेकिन चर को इंस्टेंटिएट करते समय भी किया जाता है (नीचे देखें)। समानता चिन्ह के प्रयोग से इसका प्रयोग अन्य लैंग्वेज में भी किया जाता है <code>=</code>अपितु कई ऑपरेशनों के संयोजन में भी सम्मिलित होता है <code>+</code>, <code>-</code>, <code>*</code>, <code>/</code>. प्रकार अनुमान कलन विधि सामान्यतः एकीकरण पर आधारित होते हैं।
 प्रोलॉग में:
-# एक [[ चर (प्रोग्रामिंग) |चर (प्रोग्रामिंग)]] जो अनइंस्टेंटिफाइड है—अर्थात् इस पर कोई पिछला यूनिफिकेशन नहीं किया गया था - इसे एक परमाणु, एक शब्द या किसी अन्य असंतुलित चर के साथ एकीकृत किया जा सकता है, इस प्रकार प्रभावी रूप से इसका उपनाम बन जाता है। कई आधुनिक प्रोलॉग बोलियों और [[प्रथम-क्रम तर्क|प्रथम-क्रम लॉजिक]] में एक चर को उस शब्द के साथ एकीकृत नहीं किया जा सकता है जिसमें वह सम्मिलित है; यह तथाकथित घटित जाँच है।
+# एक [[ चर (प्रोग्रामिंग) |चर (प्रोग्रामिंग)]] जो अनइंस्टेंटिफाइड है—अर्थात् इस पर कोई पिछला एकीकरण नहीं किया गया था - इसे एक परमाणु, एक शब्द या किसी अन्य असंतुलित चर के साथ एकीकृत किया जा सकता है, इस प्रकार प्रभावी रूप से इसका अलियास बन जाता है। कई आधुनिक प्रोलॉग बोलियों और [[प्रथम-क्रम तर्क|प्रथम-क्रम लॉजिक]] में एक चर को उस शब्द के साथ एकीकृत नहीं किया जा सकता है जिसमें वह सम्मिलित है; यह तथाकथित घटित जाँच है।
 # दो परमाणु तभी एकीकृत हो सकते हैं जब वे समान हों जाते है।
 # इसी प्रकार, एक पद को दूसरे पद के साथ एकीकृत किया जा सकता है यदि पदों के शीर्ष फलन प्रतीक और गुणधर्म समान हैं और यदि मापदंडों को एक साथ एकीकृत किया जा सकता है। ध्यान दें कि यह एक पुनरावर्ती व्यवहार है।
 === '''अनुप्रयोग: प्रकार अनुमान''' ===
-कार्यात्मक लैंग्वेज [[हास्केल (प्रोग्रामिंग भाषा)|हास्केल (प्रोग्रामिंग लैंग्वेज)]] और [[एमएल (प्रोग्रामिंग भाषा)|एमएल (प्रोग्रामिंग लैंग्वेज)]] सहित हिंडले-मिलनर प्रकार प्रणाली पर आधारित प्रकार प्रणालियों वाली लैंग्वेज के लिए प्रकार अनुमान के समय यूनिफिकेशन का उपयोग किया जाता है। एक ओर प्रोग्रामर को प्रत्येक फलन के लिए प्रकार की जानकारी प्रदान करने की आवश्यकता नहीं होती है, दूसरी ओर इसका उपयोग टाइपिंग त्रुटियों का पता लगाने के लिए किया जाता है। हास्केल एक्सप्रेशन <code>ट्रू  : ['x', 'y', 'z']</code> सही ढंग से टाइप नहीं किया गया है. सूची निर्माण फलन <code>(:)</code> प्रकार का है <code>a -> [a] -> [a]</code>, और पहले लॉजिक के लिए<code>ट्रू</code>बहुरूपी प्रकार चर <code>a</code> के साथ एकाकार होना होगा <code>ट्रू</code>का प्रकार <code>बूल</code>. दूसरा लॉजिक , <code>['x', 'y', 'z']</code>, प्रकार का है <code>[चार]</code>, लेकिन <code>a</code> दोनों नहीं हो सकते <code>बूल</code> और<code>चार</code> एक ही समय पर होते है.
+कार्यात्मक लैंग्वेज [[हास्केल (प्रोग्रामिंग भाषा)|हास्केल (प्रोग्रामिंग लैंग्वेज)]] और [[एमएल (प्रोग्रामिंग भाषा)|एमएल (प्रोग्रामिंग लैंग्वेज)]] सहित हिंडले-मिलनर प्रकार प्रणाली पर आधारित प्रकार प्रणालियों वाली लैंग्वेज के लिए प्रकार अनुमान के समय एकीकरण का उपयोग किया जाता है। एक ओर प्रोग्रामर को प्रत्येक फलन के लिए प्रकार की जानकारी प्रदान करने की आवश्यकता नहीं होती है, दूसरी ओर इसका उपयोग टाइपिंग त्रुटियों का पता लगाने के लिए किया जाता है। हास्केल अभिव्यक्तियों <code>ट्रू  : ['x', 'y', 'z']</code> सही ढंग से टाइप नहीं किया गया है. सूची निर्माण फलन <code>(:)</code> प्रकार का है <code>a -> [a] -> [a]</code>, और पहले लॉजिक के लिए<code>ट्रू</code>बहुरूपी प्रकार चर <code>a</code> के साथ एकाकार होना होगा <code>ट्रू</code>का प्रकार <code>बूल</code>. दूसरा लॉजिक , <code>['x', 'y', 'z']</code>, प्रकार का है <code>[चार]</code>, लेकिन <code>a</code> दोनों नहीं हो सकते <code>बूल</code> और<code>चार</code> एक ही समय पर होते है.
-प्रोलॉग के प्रकार अनुमान के लिए एक कलनविधि दिया जा सकता है:
+प्रोलॉग के प्रकार अनुमान के लिए एक कलन विधि दिया जा सकता है:
-# कोई भी प्रकार का चर किसी भी प्रकार की एक्सप्रेशन के साथ एकीकृत होता है और उस एक्सप्रेशन के लिए त्वरित होता है। एक विशिष्ट सिद्धांत इस नियम को घटित जाँच के साथ प्रतिबंधित कर सकता है।
+# कोई भी प्रकार का चर किसी भी प्रकार की अभिव्यक्तियों के साथ एकीकृत होता है और उस अभिव्यक्तियों के लिए त्वरित होता है। एक विशिष्ट सिद्धांत इस नियम को घटित जाँच के साथ प्रतिबंधित कर सकता है।
 # दो प्रकार के स्थिरांक तभी एकीकृत होते हैं जब वे एक ही प्रकार के हों जाते है।
 # दो प्रकार के निर्माण मात्र तभी एकीकृत होते हैं जब वे एक ही प्रकार के कंस्ट्रक्टर के अनुप्रयोग होते हैं और उनके सभी घटक प्रकार पुनरावर्ती रूप से एकीकृत होते हैं।
-इसकी घोषणात्मक प्रकृति के कारण यूनिफिकेशन के अनुक्रम में क्रम (सामान्यतः) महत्वहीन है।
+इसकी घोषणात्मक प्रकृति के कारण एकीकरण के अनुक्रम में क्रम (सामान्यतः) महत्वहीन है।
 ध्यान दें कि प्रथम-क्रम लॉजिक की शब्दावली में, एक परमाणु एक मूल प्रस्ताव है और प्रोलॉग शब्द के समान एकीकृत है।
 === '''अनुप्रयोग: फ़ीचर संरचना एकीकरण''' ===
-{{see also|Feature structure}}
+{{see also|फ़ीचर संरचना}}
-अभिकलनात्मक लैंग्वेज विज्ञान के विभिन्न अनुसंधान क्षेत्रों में यूनिफिकेशन के रूप में उपयोग किया गया है।<ref>Jonathan Calder, Mike Reape, and Hank Zeevat,, [https://www.aclweb.org/anthology/E89-1032 An algorithm for generation in unification categorial grammar]. In Proceedings of the 4th Conference of the European Chapter of the Association for Computational Linguistics, pages 233-240, Manchester, England (10–12 April), University of Manchester Institute of Science and Technology, 1989.</ref><ref>Graeme Hirst and David St-Onge, [http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.50.8426] Lexical chains as representations of context for the detection and correction of malapropisms, 1998.</ref>
+अभिकलनात्मक लैंग्वेज विज्ञान के विभिन्न अनुसंधान क्षेत्रों में एकीकरण के रूप में उपयोग किया गया है।<ref>Jonathan Calder, Mike Reape, and Hank Zeevat,, [https://www.aclweb.org/anthology/E89-1032 An algorithm for generation in unification categorial grammar]. In Proceedings of the 4th Conference of the European Chapter of the Association for Computational Linguistics, pages 233-240, Manchester, England (10–12 April), University of Manchester Institute of Science and Technology, 1989.</ref><ref>Graeme Hirst and David St-Onge, [http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.50.8426] Lexical chains as representations of context for the detection and correction of malapropisms, 1998.</ref>
 =='''क्रमानुसार एकीकरण'''==
@@ Line 312: / Line 309: @@
 उदाहरण के लिए एक फलन घोषणा मां: जानवर → जानवर, और एक निरंतर घोषणा लस्सी: कुत्ता मानते हुए, मां (लस्सी) शब्द पूरी प्रकार से मान्य है और इसमें जानवर की तरह है। यह जानकारी प्रदान करने के लिए कि कुत्ते की माँ बदले में एक कुत्ता है, एक और घोषणा माँ: कुत्ता → कुत्ता जारी की जा सकती है; इसे फलन ओवर लोडिंग कहा जाता है, [[प्रोग्रामिंग भाषाओं में ओवरलोडिंग|प्रोग्रामिंग लैंग्वेज में ओवरलोडिंग]] के समान हो जाता है.
-[[क्रिस्टोफ़ वाल्थर]] ने क्रम-क्रमबद्ध लॉजिक में शब्दों के लिए एक यूनिफिकेशन कलनविधि दिया जाता है, जिसके लिए किन्हीं दो घोषित प्रकारों की आवश्यकता होती है''s''<sub>1</sub>, ''s''<sub>2</sub> उनका प्रतिच्छेदन ''s''<sub>1</sub> ∩ ''s''<sub>2</sub> घोषित किया जाना भी है : यदि x<sub>1</sub> और x<sub>2</sub> सॉर्ट का एक चर है''s''<sub>1</sub>,और ''s''<sub>2</sub>, क्रमशः, समीकरण x<sub>1</sub> ≐ x<sub>2</sub> सलूशन के रूप में है {x<sub>1</sub> = x, x<sub>2</sub> = x }, जहां x: s<sub>1</sub> ∩ ''s''<sub>2</sub>.
+[[क्रिस्टोफ़ वाल्थर]] ने क्रम-क्रमबद्ध लॉजिक में शब्दों के लिए एक एकीकरण कलन विधि दिया जाता है, जिसके लिए किन्हीं दो घोषित प्रकारों की आवश्यकता होती है''s''<sub>1</sub>, ''s''<sub>2</sub> उनका प्रतिच्छेदन ''s''<sub>1</sub> ∩ ''s''<sub>2</sub> घोषित किया जाना भी है : यदि x<sub>1</sub> और x<sub>2</sub> सॉर्ट का एक चर है''s''<sub>1</sub>,और ''s''<sub>2</sub>, क्रमशः, समीकरण x<sub>1</sub> ≐ x<sub>2</sub> हल के रूप में है {x<sub>1</sub> = x, x<sub>2</sub> = x }, जहां x: s<sub>1</sub> ∩ ''s''<sub>2</sub>.
-<ref>{{cite journal|first1=Christoph|last1=Walther|author-link=Christoph Walther|title=कई-क्रमबद्ध रिज़ॉल्यूशन द्वारा शुबर्ट के स्टीमरोलर का एक यांत्रिक समाधान|journal=Artif. Intell.|volume=26|number=2|pages=217–224|url=http://www.inferenzsysteme.informatik.tu-darmstadt.de/media/is/publikationen/Schuberts_Steamroller_by_Many-Sorted_Resolution-AIJ-25-2-1985.pdf|year=1985|doi=10.1016/0004-3702(85)90029-3|access-date=2013-06-28|archive-date=2011-07-08|archive-url=https://web.archive.org/web/20110708231225/http://www.inferenzsysteme.informatik.tu-darmstadt.de/media/is/publikationen/Schuberts_Steamroller_by_Many-Sorted_Resolution-AIJ-25-2-1985.pdf|url-status=dead}}</ref>इस कलनविधि को क्लॉज-आधारित स्वचालित प्रमेय कहावत में सम्मिलित करने के पश्चात, वह एक बेंचमार्क समस्या को क्रम-क्रमबद्ध लॉजिक में अनुवाद करके हल कर सकता है, जिससे इसे परिमाण के क्रम में उबाला जा सकता है, क्योंकि कई यूनरी विधेय प्रकार में बदल जाते हैं।
+<ref>{{cite journal|first1=Christoph|last1=Walther|author-link=Christoph Walther|title=कई-क्रमबद्ध रिज़ॉल्यूशन द्वारा शुबर्ट के स्टीमरोलर का एक यांत्रिक समाधान|journal=Artif. Intell.|volume=26|number=2|pages=217–224|url=http://www.inferenzsysteme.informatik.tu-darmstadt.de/media/is/publikationen/Schuberts_Steamroller_by_Many-Sorted_Resolution-AIJ-25-2-1985.pdf|year=1985|doi=10.1016/0004-3702(85)90029-3|access-date=2013-06-28|archive-date=2011-07-08|archive-url=https://web.archive.org/web/20110708231225/http://www.inferenzsysteme.informatik.tu-darmstadt.de/media/is/publikationen/Schuberts_Steamroller_by_Many-Sorted_Resolution-AIJ-25-2-1985.pdf|url-status=dead}}</ref>इस कलन विधि को क्लॉज-आधारित स्वचालित प्रमेय कहावत में सम्मिलित करने के पश्चात, वह एक बेंचमार्क समस्या को क्रम-क्रमबद्ध लॉजिक में अनुवाद करके हल कर सकता है, जिससे इसे परिमाण के क्रम में उबाला जा सकता है, क्योंकि कई यूनरी विधेय प्रकार में बदल जाते हैं।
 [[पैरामीट्रिक बहुरूपता]] की अनुमति देने के लिए स्मोल्का ने क्रम-क्रमबद्ध लॉजिक को सामान्यीकृत किया जाता है।
-<ref>{{cite conference|first1=Gert|last1=Smolka|title=पॉलिमॉर्फिकली ऑर्डर-सॉर्टेड प्रकारों के साथ लॉजिक प्रोग्रामिंग|conference=Int. Workshop Algebraic and Logic Programming|publisher=Springer|series=LNCS|volume=343|pages=53–70|date=Nov 1988|url=https://link.springer.com/content/pdf/10.1007/3-540-50667-5_58.pdf|doi=10.1007/3-540-50667-5_58}}</ref>उनके ढांचे में उप-घोषणाएँ सम्मिश्र प्रकार की एक्सप्रेशन के लिए प्रचारित की जाती हैं।
+<ref>{{cite conference|first1=Gert|last1=Smolka|title=पॉलिमॉर्फिकली ऑर्डर-सॉर्टेड प्रकारों के साथ लॉजिक प्रोग्रामिंग|conference=Int. Workshop Algebraic and Logic Programming|publisher=Springer|series=LNCS|volume=343|pages=53–70|date=Nov 1988|url=https://link.springer.com/content/pdf/10.1007/3-540-50667-5_58.pdf|doi=10.1007/3-540-50667-5_58}}</ref>उनके ढांचे में उप-घोषणाएँ सम्मिश्र प्रकार की अभिव्यक्तियों के लिए प्रचारित की जाती हैं।
 एक प्रोग्रामिंग उदाहरण के रूप में एक पैरामीट्रिक सॉर्ट सूची (X) घोषित की जा सकती है (टेम्प्लेट (C++)# फलन टेम्पलेट्स |C++ टेम्प्लेट में X एक प्रकार का पैरामीटर है), और एक सबसॉर्ट घोषणा से int ⊆ संबंध सूची फ़्लोट करें (int ) ⊆ सूची (फ्लोट) का स्वचालित रूप से अनुमान लगाया जाता है, जिसका अर्थ है कि पूर्णांकों की प्रत्येक सूची भी फ्लोट्स की एक सूची है।
@@ Line 324: / Line 321: @@
 श्मिट-शाउß ने शब्द घोषणाओं की अनुमति देने के लिए क्रम-क्रमबद्ध लॉजिक को सामान्यीकृत किया।
 <ref>{{cite book|first1=Manfred|last1=Schmidt-Schauß|title=टर्म घोषणाओं के साथ ऑर्डर-सॉर्टेड लॉजिक के कम्प्यूटेशनल पहलू|publisher=Springer|series=[[Lecture Notes in Artificial Intelligence]] (LNAI)|volume=395|date=Apr 1988}}</ref>
-उदाहरण के तौर पर, उपवर्ग घोषणाओं को सम ⊆ int और विषम ⊆ int मानते हुए, एक शब्द घोषणा जैसे ∀ i : int। (i + i): पूर्णांक जोड़ की एक संपत्ति घोषित करने की भी अनुमति देता है जिसे सामान्य ओवरलोडिंग द्वारा व्यक्त नहीं किया जा सकता है।
+उदाहरण के तौर पर, उपवर्ग घोषणाओं को सम ⊆ int और विषम ⊆ int मानते हुए, एक शब्द घोषणा जैसे ∀ i : int। (i + i): पूर्णांक जोड़ की एक गुणधर्म घोषित करने की भी अनुमति देता है जिसे सामान्य ओवरलोडिंग द्वारा व्यक्त नहीं किया जा सकता है।
 =='''अनंत पदों का एकीकरण'''==
 {{expand section|date=December 2021}}
 अनंत पेड़ों पर पृष्ठभूमि:
-* {{cite journal| author=B. Courcelle| author-link=Bruno Courcelle| title=अनंत वृक्षों के मौलिक गुण| journal=Theoret. Comput. Sci.| year=1983| volume=25| issue=2| pages=95–169| doi=10.1016/0304-3975(83)90059-2| doi-access=free}}
+* {{cite journal| author=बी कौरसेल| author-link=Bruno Courcelle| title=अनंत ट्री के मौलिक गुण| journal=सैद्धांतिक संगणना विज्ञान.| year=1983| volume=25| issue=2| pages=95–169| doi=10.1016/0304-3975(83)90059-2| doi-access=free}}
-* {{cite book| author=Michael J. Maher| chapter=Complete Axiomatizations of the Algebras of Finite, Rational and Infinite Trees| title=प्रोक. आईईईई तीसरा वार्षिक संगोष्ठी। कंप्यूटर विज्ञान में तर्क पर, एडिनबर्ग|date=Jul 1988| pages=348–357}}
+* माइकल जे. महर (जुलाई 1988)"परिमित, तर्कसंगत और अनंत पेड़ों के बीजगणित के पूर्ण स्वयंसिद्ध!"''प्रोक. आईईईई तीसरा वार्षिक संगोष्ठी'' पर कंप्यूटर विज्ञान में तर्क, एडिनबर्ग.पृ. 348-357
 * {{cite journal|author1=Joxan Jaffar |author2=Peter J. Stuckey | title=अनंत वृक्ष तर्क प्रोग्रामिंग के शब्दार्थ| journal=Theoretical Computer Science| year=1986| volume=46| pages=141–158| doi=10.1016/0304-3975(86)90027-7| doi-access=free}}
-यूनिफिकेशन एल्गोरिथ्म, प्रोलॉग II:
+एकीकरण कलन विधि , प्रोलॉग II:
-* {{cite book| author=A. Colmerauer| author-link=Alain Colmerauer|title=प्रोलॉग और अनंत पेड़| year=1982| publisher=Academic Press|editor1=K.L. Clark |editor2=S.-A. Tarnlund }}
+* {{cite book| author=ए कोलमेरौएर| author-link=Alain Colmerauer|title=प्रोलॉग और अनंत पेड़| year=1982| publisher=अकादमिक प्रेस|editor1=के.एल. क्लार्क |editor2=एस.-ए. टार्नलुंड }}
-* {{cite book| author=Alain Colmerauer| chapter=Equations and Inequations on Finite and Infinite Trees| title=प्रोक. इंट. कॉन्फ़. पांचवीं पीढ़ी के कंप्यूटर सिस्टम पर| year=1984| pages=85–99| editor=ICOT}}
+* एलेन कोलम्योर (1984)"परिमित और अनंत पेड़ों पर समीकरण और असमानताएं"आईसीयू (एडी) में प्रक्रिया समझौता। पांचवीं पीढ़ी कंप्यूटर सिस्टम पर पृ. 85-99 अनुप्रयोग।
-अनुप्रयोग:
+* {{cite journal|author1=फ्रांसिस जियानेसिनी |author2=जैक्स कोहेन | title=प्रोलॉग के अनंत पेड़ों का उपयोग करके पार्सर जेनरेशन और व्याकरण हेरफेर| journal=जर्नल ऑफ़ लॉजिक प्रोग्रामिंग| year=1984| volume=1|issue=3 | pages=253–265| doi=10.1016/0743-1066(84)90013-X| doi-access=free}}
-* {{cite journal|author1=Francis Giannesini |author2=Jacques Cohen | title=प्रोलॉग के अनंत पेड़ों का उपयोग करके पार्सर जेनरेशन और व्याकरण हेरफेर| journal=Journal of Logic Programming| year=1984| volume=1|issue=3 | pages=253–265| doi=10.1016/0743-1066(84)90013-X| doi-access=free}}
 =='''ई-एकीकरण'''==
-ई-यूनिफिकेशन [[समीकरण]] के दिए गए सेट का सलूशन खोजने की समस्या है.
+ई- एकीकरण [[समीकरण]] के दिए गए समुच्चय का हल खोजने की समस्या है.
 कुछ समीकरणात्मक पृष्ठभूमि ज्ञान E को ध्यान में रखते हुए।
-उत्तरार्द्ध को सार्वभौमिक [[समानता]] के एक सेट के रूप में दिया गया है।
+उत्तरार्द्ध को सार्वभौमिक [[समानता]] के एक समुच्चय के रूप में दिया गया है।
-कुछ विशेष सेट E के लिए समीकरण हल करने वाले कलनविधि (उर्फ ''ई-यूनिफिकेशन एल्गोरिदम'') तैयार किए गए हैं;
+कुछ विशेष समुच्चय E के लिए समीकरण हल करने वाले कलन विधि (उर्फ ''ई- एकीकरण एल्गोरिदम'') तैयार किए गए हैं;
-दूसरों के लिए यह सिद्ध हो चुका है कि ऐसा कोई कलनविधि उपलब्ध नहीं हो सकता है।
+दूसरों के लिए यह सिद्ध हो चुका है कि ऐसा कोई कलन विधि उपलब्ध नहीं हो सकता है।
 उदाहरण के लिए, यदि {{mvar|a}} और {{mvar|b}} विशिष्ट स्थिरांक हैं,
-[[समीकरण]] {{tmath|x * a \doteq y * b}} का कोई सलूशन नहीं है.
+[[समीकरण]] {{tmath|x * a \doteq y * b}} का कोई हल नहीं है.
-विशुद्ध [[वाक्यात्मक एकीकरण|सिंटैक्टिक]] यूनिफिकेशन में संबंध हो जाता है
+विशुद्ध वाक्यात्मकएकीकरण में संबंध हो जाता है
 जहां संचालक के बारे में कुछ भी पता नहीं चल पाया है {{tmath|*}}.
@@ Line 372: / Line 368: @@
 | {{tmath|b * a}}
 |
-| प्रतिस्थापन आवेदन द्वारा
+| प्रतिस्थापन अनुप्रयोग द्वारा
 |-
 | {{=}}
@@ Line 382: / Line 378: @@
 | {{tmath|y * b}}
 | {{math|{{mset|''x'' ↦ ''b'', ''y'' ↦ ''a''}}}}
-| (विपरीत) प्रतिस्थापन आवेदन द्वारा
+| (विपरीत) प्रतिस्थापन अनुप्रयोग द्वारा
 |}
 पृष्ठभूमि ज्ञान E की क्रम परिवर्तनशीलता बता सकता है {{tmath|*}} सार्वभौम समानता द्वारा{{tmath|1=u * v = v * u}} सभी के लिए {{math|''u'', ''v''}} .
-===विशेष पृष्ठभूमि ज्ञान सेट E===
+===विशेष पृष्ठभूमि ज्ञान समुच्चय E===
 {|
 |+ '''Used naming conventions'''
@@ Line 394: / Line 390: @@
 | {{tmath|(u*v)*w}}
 | align="center" | '''{{mvar|A}}'''
-| Associativity of {{tmath|*}}
+| की संबद्धता {{tmath|*}}
 |-
 | {{math|∀ ''u'',''v'':}}
@@ Line 401: / Line 397: @@
 | {{tmath|v*u}}
 | align="center" | '''{{mvar|C}}'''
-| Commutativity of {{tmath|*}}
+| की क्रमपरिवर्तनशीलता {{tmath|*}}
 |-
 | {{math|∀ ''u'',''v'',''w'':}}
@@ Line 408: / Line 404: @@
 | {{tmath|u*v+u*w}}
 | align="center" | '''{{mvar|D<sub>l</sub>}}'''
-| Left distributivity of {{tmath|*}} over {{tmath|+}}
+| का वाम वितरण
+∗
+ऊपर
++
 |-
 | {{math|∀ ''u'',''v'',''w'':}}
@@ Line 415: / Line 416: @@
 | {{tmath|v*u+w*u}}
 | align="center" | '''{{mvar|D<sub>r</sub>}}'''
-| Right distributivity of {{tmath|*}} over {{tmath|+}}
+| का सही वितरण
+∗
+ऊपर
++
 |-
 | {{math|∀ ''u'':}}
@@ Line 422: / Line 428: @@
 | {{mvar|u}}
 | align="center" | '''{{mvar|I}}'''
-| Idempotence of {{tmath|*}}
+| नपुंसकताof {{tmath|*}}
 |-
 | {{math|∀ ''u'':}}
@@ Line 429: / Line 435: @@
 | {{mvar|u}}
 | align="center" | '''{{mvar|N<sub>l</sub>}}'''
-| Left neutral element {{mvar|n}} with respect to {{tmath|*}}
+| के संबंध में तटस्थ तत्व n छोड़ दिया {{tmath|*}}
 |-
 | {{math|∀ ''u'':}}
@@ Line 436: / Line 442: @@
 | {{mvar|u}}
 | align="center" | &nbsp; &nbsp; '''{{mvar|N<sub>r</sub>}}''' &nbsp; &nbsp;
-| Right neutral element {{mvar|n}} with respect to {{tmath|*}}
+| के संबंध में सही तटस्थ तत्व n
+<nowiki>**</nowiki> {{tmath|*}}
 |}
-ऐसा कहा जाता है कि यूनिफिकेशन एक सिद्धांत के लिए निर्णायक होता है, यदि इसके लिए एक यूनिफिकेशन कलनविधि तैयार किया गया है, जो किसी भी इनपुट समस्या के लिए समाप्त हो जाता है।
+ऐसा कहा जाता है कि एकीकरण एक सिद्धांत के लिए निर्णायक होता है, यदि इसके लिए एक एकीकरण कलन विधि तैयार किया गया है, जो किसी भी इनपुट समस्या के लिए समाप्त हो जाता है।
-ऐसा कहा जाता है कि यूनिफिकेशन एक सिद्धांत के लिए अर्ध-निर्णायक है, यदि इसके लिए एक यूनिफिकेशन कलनविधि तैयार किया गया है, जो किसी भी हल करने योग्य इनपुट समस्या के लिए समाप्त हो जाता है, लेकिन एक अघुलनशील इनपुट समस्या के सलूशन के लिए निरंतर के लिए खोज जारी रख सकता है।
+ऐसा कहा जाता है कि एकीकरण एक सिद्धांत के लिए अर्ध-निर्णायक है, यदि इसके लिए एक एकीकरण कलन विधि तैयार किया गया है, जो किसी भी हल करने योग्य इनपुट समस्या के लिए समाप्त हो जाता है, लेकिन एक अघुलनशील इनपुट समस्या के हल के लिए निरंतर के लिए खोज जारी रख सकता है।
-निम्नलिखित सिद्धांतों के लिए 'यूनिफिकेशन निर्णायक है':
+निम्नलिखित सिद्धांतों के लिए ' एकीकरण निर्णायक है':
 *'{{mvar|A}}<ref>[[Gordon D. Plotkin]], ''Lattice Theoretic Properties of Subsumption'', Memorandum MIP-R-77, Univ. Edinburgh, Jun 1970</ref>
 *{{mvar|A}},{{mvar|C}}<ref>[[Mark E. Stickel]], ''A Unification Algorithm for Associative-Commutative Functions'', J. Assoc. Comput. Mach., vol.28, no.3, pp. 423–434, 1981</ref>
@@ Line 452: / Line 459: @@
 * एबेलियन समूह, यदि हस्ताक्षर को यादृच्छिक ढंग से अतिरिक्त प्रतीकों द्वारा विस्तारित किया गया हो (लेकिन स्वयंसिद्ध नहीं)<ref name="Baader and Snyder 2001, p. 486">Baader and Snyder (2001), p. 486.</ref>
 * क्रिपके शब्दार्थ#पत्राचार और पूर्णता [[मोडल बीजगणित]]<ref>F. Baader and S. Ghilardi, ''[https://web.archive.org/web/20171223215706/https://pdfs.semanticscholar.org/492e/9f03ab7abd043ed0167dc7309552d21a88ef.pdf Unification in modal and description logics]'', Logic Journal of the IGPL 19 (2011), no.&nbsp;6, pp.&nbsp;705–730.</ref>
-निम्नलिखित सिद्धांतों के लिए यूनिफिकेशन अर्ध-निर्णायक है:
+निम्नलिखित सिद्धांतों के लिए एकीकरण अर्ध-निर्णायक है:
 *{{mvar|A}},{{mvar|D<sub>l</sub>}}{{mvar|,}}{{mvar|D<sub>r</sub>}}<ref>P. Szabo, ''Unifikationstheorie erster Ordnung'' (''First Order Unification Theory''), Thesis, Univ. Karlsruhe, West Germany, 1982</ref>
 *{{mvar|A}},{{mvar|C}},{{mvar|D<sub>l</sub>}}<ref group=note name="LRequivC"/><ref>Jörg H. Siekmann, ''Universal Unification'', Proc. 7th Int. Conf. on Automated Deduction, Springer LNCS vol.170, pp. 1–42, 1984</ref>
@@ Line 500: / Line 507: @@
 | &nbsp; &nbsp; '''imitate'''
 |}
-''G'' से प्रारंभ करके हल की जाने वाली यूनिफिकेशन समस्या और S पहचान प्रतिस्थापन है, नियमों को गैर-नियतात्मक रूप से लागू किया जाता है, जब तक कि खाली सेट वास्तविक ''G'' के रूप में प्रकट नहीं होता है, इस स्थिति में वास्तविक S एक एकीकृत प्रतिस्थापन है। आदेश के आधार पर पैरामॉड्यूलेशन नियम लागू होते हैं, ''G'' से वास्तविक समीकरण की पसंद पर और ''R'' की पसंद पर{{'}}के नियमों में परिवर्तन, विभिन्न संगणना पथ संभव हैं। मात्र कुछ ही सलूशन की ओर ले जाते हैं, जबकि अन्य G ≠ {} पर समाप्त होते हैं, जहां कोई और नियम लागू नहीं होता है. (जैसे G = { f(...) ≐ g(...) })।
+''G'' से प्रारंभ करके हल की जाने वाली एकीकरण समस्या और S पहचान प्रतिस्थापन है, नियमों को गैर-नियतात्मक रूप से प्रयुक्त किया जाता है, जब तक कि खाली समुच्चय वास्तविक ''G'' के रूप में प्रकट नहीं होता है, इस स्थिति में वास्तविक S एक एकीकृत प्रतिस्थापन है। आदेश के आधार पर पैरामॉड्यूलेशन नियम प्रयुक्त होते हैं, ''G'' से वास्तविक समीकरण की पसंद पर और ''R'' की पसंद पर{{'}}के नियमों में परिवर्तन, विभिन्न संगणना पथ संभव हैं। मात्र कुछ ही हल की ओर ले जाते हैं, जबकि अन्य G ≠ {} पर समाप्त होते हैं, जहां कोई और नियम प्रयुक्त नहीं होता है. (जैसे G = { f(...) ≐ g(...) })।
 {| style="border: 1px solid darkgray;"
@@ Line 513: / Line 520: @@
 | → ''x''.''app''(''y'',''z'')
 |}
-उदाहरण के लिए एक शब्द रीराइट सिस्टम ''R'' का उपयोग विपक्ष और शून्य से निर्मित सूचियों के परिशिष्ट ऑपरेटर को परिभाषित करने के लिए किया जाता है; जहां संक्षिप्तता के लिए cons(x,y) को इन्फ़िक्स नोटेशन में x.y के रूप में लिखा जाता है; जैसे ऐप(a.b.nil,c.d.nil) → a.app(b.nil,c.d.nil) → a.b.app(nil,c.d.nil) → a.b.c.d.nil सूचियों a.b.nil और c.d.nil के संयोजन को प्रदर्शित करता है, पुनर्लेखन नियम 2 का उपयोग करते हुए, 2, और 1. R के अनुरूप समीकरण सिद्धांत E, R का सर्वांगसम समापन है, दोनों को शर्तों पर द्विआधारी संबंध के रूप में देखा जाता है।
+उदाहरण के लिए एक शब्द रीराइट प्रणाली ''R'' का उपयोग विपक्ष और शून्य से निर्मित सूचियों के परिशिष्ट ऑपरेटर को परिभाषित करने के लिए किया जाता है; जहां संक्षिप्तता के लिए cons(x,y) को इन्फ़िक्स नोटेशन में x.y के रूप में लिखा जाता है; जैसे ऐप(a.b.nil,c.d.nil) → a.app(b.nil,c.d.nil) → a.b.app(nil,c.d.nil) → a.b.c.d.nil सूचियों a.b.nil और c.d.nil के संयोजन को प्रदर्शित करता है, पुनर्लेखन नियम 2 का उपयोग करते हुए, 2, और 1. R के अनुरूप समीकरण सिद्धांत E, R का सर्वांगसम समापन है, दोनों को शर्तों पर द्विआधारी संबंध के रूप में देखा जाता है।
-उदाहरण के लिए, ऐप(a.b.nil,c.d.nil) ≡ a.b.c.d.nil ≡ ऐप(a.b.c.d.nil,nil)। पैरामोड्यूलेशन कलनविधि उदाहरण ''R'' के साथ दिए जाने पर उस E के संबंध में समीकरणों के सलूशन की गणना करता है।
+उदाहरण के लिए, ऐप(a.b.nil,c.d.nil) ≡ a.b.c.d.nil ≡ ऐप(a.b.c.d.nil,nil)। पैरामोड्यूलेशन कलन विधि उदाहरण ''R'' के साथ दिए जाने पर उस E के संबंध में समीकरणों के हल की गणना करता है।
-यूनिफिकेशन समस्या {app(x,app(y,x)) ≐ a.a.nil } के लिए एक सफल उदाहरण गणना पथ नीचे दिखाया गया है। परिवर्तनीय नाम टकराव से बचने के लिए, नियम परिवर्तन द्वारा उनके उपयोग से पहले हर बार पुनर्लेखन नियमों का लगातार नाम बदला जाता है; ''v''<sub>2</sub>, ''v''<sub>3</sub>, ... इस उद्देश्य के लिए कंप्यूटर-जनित परिवर्तनीय नाम हैं। प्रत्येक पंक्ति में, G से चुना गया समीकरण लाल रंग में हाइलाइट किया गया है। हर बार जब उत्परिवर्तित नियम लागू किया जाता है, तो चुने गए पुनर्लेखन नियम (1 या 2) को कोष्ठक में दर्शाया जाता है। अंतिम पंक्ति से एकीकृत प्रतिस्थापन S = {y ↦ nil, x ↦ a.nil } प्राप्त किया जा सकता है। वास्तव में,
+एकीकरण समस्या {app(x,app(y,x)) ≐ a.a.nil } के लिए एक सफल उदाहरण गणना पथ नीचे दिखाया गया है। परिवर्तनीय नाम टकराव से बचने के लिए, नियम परिवर्तन द्वारा उनके उपयोग से पहले हर बार पुनर्लेखन नियमों का लगातार नाम बदला जाता है; ''v''<sub>2</sub>, ''v''<sub>3</sub>, ... इस उद्देश्य के लिए कंप्यूटर-जनित परिवर्तनीय नाम हैं। प्रत्येक पंक्ति में, G से चुना गया समीकरण लाल रंग में हाइलाइट किया गया है। हर बार जब उत्परिवर्तित नियम प्रयुक्त किया जाता है, तो चुने गए पुनर्लेखन नियम (1 या 2) को कोष्ठक में दर्शाया जाता है। अंतिम पंक्ति से एकीकृत प्रतिस्थापन S = {y ↦ nil, x ↦ a.nil } प्राप्त किया जा सकता है। वास्तव में,
-ऐप(x,ऐप(y,x)) {y↦nil, x↦ a.nil } = ऐप(a.nil,app(nil,a.nil)) ≡ ऐप(a.nil,a.nil) ≡ a.app(nil,a.nil) ≡ a.a.nil दी गई समस्या का सलूशन करता है।
+ऐप(x,ऐप(y,x)) {y↦nil, x↦ a.nil } = ऐप(a.nil,app(nil,a.nil)) ≡ ऐप(a.nil,a.nil) ≡ a.app(nil,a.nil) ≡ a.a.nil दी गई समस्या का हल करता है।
 दूसरा सफल संगणना पथ, जिसे mutate(1), mutate(2), mutate(2), mutate(1) चुनकर प्राप्त किया जा सकता है, प्रतिस्थापन की ओर ले जाता है S = { y ↦ a.a.nil, x ↦ nil }; यह यहां नहीं दिखाया गया है. कोई अन्य मार्ग सफलता की ओर नहीं ले जाता।
 {| class="wikitable"
-|+ Example unifier computation
+|+ उदाहरण एकीकरण अभिकलन
 |-
-! Used rule !!  !! ''G'' !! ''S''
+! प्रयुक्त नियम !! !! ''G'' !! ''S''
 |-
 | ||
@@ Line 532: / Line 539: @@
 | {}
 |-
-| mutate(2) || ⇒
+| म्यूटेट(2) || ⇒
 | { ''x'' ≐ ''v''<sub>2</sub>.''v''<sub>3</sub>, ''app''(''y'',''x'') ≐ ''v''<sub>4</sub>, {{color|red|''v''<sub>2</sub>.''app''(''v''<sub>3</sub>,''v''<sub>4</sub>) ≐ ''a''.''a''.''nil''}} }
 | {}
 |-
-| decompose || ⇒
+| डीकोम्पोस || ⇒
 | { {{color|red|''x'' ≐ ''v''<sub>2</sub>.''v''<sub>3</sub>}}, ''app''(''y'',''x'') ≐ ''v''<sub>4</sub>, ''v''<sub>2</sub> ≐ ''a'', ''app''(''v''<sub>3</sub>,''v''<sub>4</sub>) ≐ ''a''.''nil'' }
 | {}
 |-
-| eliminate || ⇒
+| एलिमिनेट || ⇒
 | { ''app''(''y'',''v''<sub>2</sub>.''v''<sub>3</sub>) ≐ ''v''<sub>4</sub>, {{color|red|''v''<sub>2</sub> ≐ ''a''}}, ''app''(''v''<sub>3</sub>,''v''<sub>4</sub>) ≐ ''a''.''nil'' }
 | { ''x'' ↦ ''v''<sub>2</sub>.''v''<sub>3</sub> }
 |-
-| eliminate || ⇒
+| एलिमिनेट || ⇒
 | { {{color|red|''app''(''y'',''a''.''v''<sub>3</sub>) ≐ ''v''<sub>4</sub>}}, ''app''(''v''<sub>3</sub>,''v''<sub>4</sub>) ≐ ''a''.''nil'' }
 | { ''x'' ↦ ''a''.''v''<sub>3</sub> }
@@ Line 552: / Line 559: @@
 | { ''x'' ↦ ''a''.''v''<sub>3</sub> }
 |-
-| eliminate || ⇒
+| एलिमिनेट || ⇒
 | { {{color|red|''y'' ≐ ''nil''}}, ''a''.''v''<sub>3</sub> ≐ ''v''<sub>4</sub>, ''app''(''v''<sub>3</sub>,''v''<sub>4</sub>) ≐ ''a''.''nil'' }
 | { ''x'' ↦ ''a''.''v''<sub>3</sub> }
 |-
-| eliminate || ⇒
+| एलिमिनेट || ⇒
 | { ''a''.''v''<sub>3</sub> ≐ ''v''<sub>4</sub>, {{color|red|''app''(''v''<sub>3</sub>,''v''<sub>4</sub>) ≐ ''a''.''nil''}} }
 | { ''y'' ↦ ''nil'', ''x'' ↦ ''a''.''v''<sub>3</sub> }
 |-
-| mutate(1) || ⇒
+| म्यूटेट(1) || ⇒
 | { ''a''.''v''<sub>3</sub> ≐ ''v''<sub>4</sub>, ''v''<sub>3</sub> ≐ ''nil'', {{color|red|''v''<sub>4</sub> ≐ ''v''<sub>6</sub>}}, ''v''<sub>6</sub> ≐ ''a''.''nil'' }
 | { ''y'' ↦ ''nil'', ''x'' ↦ ''a''.''v''<sub>3</sub> }
 |-
-| eliminate || ⇒
+| एलिमिनेट || ⇒
 | { ''a''.''v''<sub>3</sub> ≐ ''v''<sub>4</sub>, {{color|red|''v''<sub>3</sub> ≐ ''nil''}}, ''v''<sub>4</sub> ≐ ''a''.''nil'' }
 | { ''y'' ↦ ''nil'', ''x'' ↦ ''a''.''v''<sub>3</sub> }
 |-
-| eliminate || ⇒
+| एलिमिनेट || ⇒
 | { ''a''.''nil'' ≐ ''v''<sub>4</sub>, {{color|red|''v''<sub>4</sub> ≐ ''a''.''nil''}} }
 | { ''y'' ↦ ''nil'', ''x'' ↦ ''a''.''nil'' }
 |-
-| eliminate || ⇒
+| एलिमिनेट || ⇒
 | { {{color|red|''a''.''nil'' ≐ ''a''.''nil''}} }
 | { ''y'' ↦ ''nil'', ''x'' ↦ ''a''.''nil'' }
 |-
-| decompose || ⇒
+| डीकोम्पोस || ⇒
 | { {{color|red|''a'' ≐ ''a''}}, ''nil'' ≐ ''nil'' }
 | { ''y'' ↦ ''nil'', ''x'' ↦ ''a''.''nil'' }
 |-
-| decompose || ⇒
+| डीकोम्पोस || ⇒
 | { {{color|red|''nil'' ≐ ''nil''}} }
 | { ''y'' ↦ ''nil'', ''x'' ↦ ''a''.''nil'' }
 |-
-| decompose &nbsp; &nbsp; || ⇒ &nbsp; &nbsp;
+| डीकोम्पोस || ⇒ &nbsp; &nbsp;
 | {}
 | { ''y'' ↦ ''nil'', ''x'' ↦ ''a''.''nil'' }
@@ Line 598: / Line 605: @@
 एक संकीर्ण चरण (cf. चित्र) के रूप में सम्मिलित है
 * वर्तमान पद का एक गैर-परिवर्तनीय उपपद चुनना है,
-* आर से एक नियम के बाईं ओर इसे [[वाक्यात्मक रूप से एकीकृत करना|सिंटैक्टिक रूप से एकीकृत करना]], और
+* आर से एक नियम के बाईं ओर इसे [[वाक्यात्मक रूप से एकीकृत करना|वाक्यात्मकरूप से एकीकृत करना]], और
 * तात्कालिक नियम के दाहिने हाथ को तात्कालिक शब्द में बदलना होता है।
-फॉर्मल रूप से, यदि {{math|''l'' → ''r''}} आर से पुनर्लेखन नियम की एक पुनर्नामित प्रति है, जिसमें शब्द एस और उपपद के साथ कोई चर समान नहीं है {{math|''s''{{!}}<sub>''p''</sub>}} एक चर नहीं है और इसके साथ एकीकृत किया जा सकता है {{mvar|l}} प्रथम-क्रम शब्दों के #सिंटैक्टिक यूनिफिकेशन के माध्यम से {{mvar|σ}}, तब {{mvar|s}} को इस शब्द तक सीमित किया जा सकता है {{math|1=''t'' = ''sσ''[''rσ'']<sub>''p''</sub>}}, अर्थात पद के लिए {{mvar|sσ}}, पी पर सबटर्म के साथ टर्म (लॉजिक)#ऑपरेशन्स विद टर्म्स बाय {{mvar|rσ}}. वह स्थिति जिसमें s को t तक सीमित किया जा सकता है, सामान्यतः s ↝ t के रूप में निरूपित की जाती है।
+फॉर्मल रूप से, यदि {{math|''l'' → ''r''}} आर से पुनर्लेखन नियम की एक पुनर्नामित प्रति है, जिसमें शब्द एस और उपपद के साथ कोई चर समान नहीं है {{math|''s''{{!}}<sub>''p''</sub>}} एक चर नहीं है और इसके साथ एकीकृत किया जा सकता है {{mvar|l}} प्रथम-क्रम शब्दों के # वाक्यात्मकएकीकरण के माध्यम से {{mvar|σ}}, तब {{mvar|s}} को इस शब्द तक सीमित किया जा सकता है {{math|1=''t'' = ''sσ''[''rσ'']<sub>''p''</sub>}}, अर्थात पद के लिए {{mvar|sσ}}, पी पर सबटर्म के साथ टर्म (लॉजिक)#ऑपरेशन्स विद टर्म्स बाय {{mvar|rσ}}. वह स्थिति जिसमें s को t तक सीमित किया जा सकता है, सामान्यतः s ↝ t के रूप में निरूपित की जाती है।
-सहज रूप से, संकीर्ण चरणों का एक क्रम टी<sub>1</sub> ↝ टी<sub>2</sub> ↝ ... ↝ टी<sub>''n''</sub> इसे पुनः लिखने के चरणों के अनुक्रम के रूप में सोचा जा सकता है<sub>1</sub> → टी<sub>2</sub> → ... → टी<sub>''n''</sub>, लेकिन प्रारंभिक पद t के साथ<sub>1</sub> प्रत्येक प्रयुक्त नियम को लागू करने के लिए आवश्यकतानुसार इसे और अधिक त्वरित किया जा रहा है।
+सहज रूप से, संकीर्ण चरणों का एक क्रम टी<sub>1</sub> ↝ टी<sub>2</sub> ↝ ... ↝ टी<sub>''n''</sub> इसे पुनः लिखने के चरणों के अनुक्रम के रूप में सोचा जा सकता है<sub>1</sub> → टी<sub>2</sub> → ... → टी<sub>''n''</sub>, लेकिन प्रारंभिक पद t के साथ<sub>1</sub> प्रत्येक प्रयुक्त नियम को प्रयुक्त करने के लिए आवश्यकतानुसार इसे और अधिक त्वरित किया जा रहा है।
 #एकतरफा पैरामॉड्यूलेशन उदाहरण पैरामॉड्यूलेशन गणना निम्नलिखित संकीर्ण अनुक्रम से मेल खाती है (↓ यहां तात्कालिकता का संकेत है):
@@ Line 622: / Line 629: @@
 |     ||         ||         ||         ||     ||                   ||                   ||     ||             ||                   ||  ''v''<sub>2</sub>.''app''( || ''nil'' || ,''v''<sub>2</sub>. || ''nil'' || )  ||  →  ||  ''v''<sub>2</sub>.''v''<sub>2</sub>.''nil''
 |}
-अंतिम पद, वी<sub>2</sub>।में<sub>2</sub>.nil को मूल दाहिनी ओर के शब्द a.a.nil के साथ सिंटैक्टिक रूप से एकीकृत किया जा सकता है।
+अंतिम पद, वी<sub>2</sub>।में<sub>2</sub>.nil को मूल दाहिनी ओर के शब्द a.a.nil के साथ वाक्यात्मकरूप से एकीकृत किया जा सकता है।
 सिकुड़ती लेम्मा<ref>{{cite book| author=Fay| chapter=First-Order Unification in an Equational Theory| title=Proc. 4th Workshop on Automated Deduction| year=1979| pages=161–167}}</ref> यह सुनिश्चित करता है कि जब भी किसी शब्द के उदाहरण को एक अभिसरण शब्द पुनर्लेखन प्रणाली द्वारा किसी शब्द t में फिर से लिखा जा सकता है, तो s और t को संकुचित किया जा सकता है और एक शब्द में फिर से लिखा जा सकता है {{math|1=''s{{prime}}''}} और {{math|1=''t{{prime}}''}}, क्रमशः, ऐसे कि {{math|1=''t{{prime}}''}} का एक उदाहरण है {{math|1=''s{{prime}}''}}.
@@ Line 629: / Line 636: @@
 ==उच्च-क्रम एकीकरण==
-[[File:Goldfarb4a svg.svg|thumb|300px|गोल्डफ़ार्ब में<ref name="Goldfarb.1981"/>हिल्बर्ट की 10वीं समस्या को दूसरे क्रम की एकीकरणीयता, समीकरण में घटाना <math>X_1 * X_2 = X_3</math> फलन चर के साथ चित्रित यूनिफिकेशन समस्या से मेल खाता है <math>F_i</math> तदनुसार <math>X_i</math> और <math>G</math> [[ताजा चर]].]]कई अनुप्रयोगों के लिए प्रथम-क्रम शब्दों के अतिरिक्त टाइप किए गए लैम्ब्डा-शब्दों के यूनिफिकेशन पर विचार करने की आवश्यकता होती है। इस प्रकार के यूनिफिकेशन को अधिकांशतः उच्च-क्रम यूनिफिकेशन कहा जाता है। उच्च-क्रम यूनिफिकेशन [[अनिर्णीत समस्या]] है,<ref name="Goldfarb.1981">{{cite journal| author=Warren D. Goldfarb| author-link=Warren D. Goldfarb| title=द्वितीय-क्रम एकीकरण समस्या की अनिर्णयता| journal=TCS| year=1981| volume=13| issue=2| pages=225–230| doi=10.1016/0304-3975(81)90040-2| doi-access=free}}</ref><ref>{{cite journal| author=Gérard P. Huet| title=तीसरे क्रम के तर्क में एकीकरण की अनिश्चितता| journal=Information and Control| year=1973| volume=22| issue=3| pages=257–267 |doi=10.1016/S0019-9958(73)90301-X| doi-access=free}}</ref><ref>Claudio Lucchesi: The Undecidability of the Unification Problem for Third Order Languages (Research Report CSRR 2059; Department of Computer Science, University of Waterloo, 1972)</ref> और ऐसी यूनिफिकेशन समस्याओं में अधिकांश सामान्य एकीकरणकर्ता नहीं होते हैं। उदाहरण के लिए, यूनिफिकेशन समस्या { f(a,b,a) ≐ d(b,a,c) }, जहां एकमात्र चर f है, में है
+[[File:Goldfarb4a svg.svg|thumb|300px|गोल्डफ़ार्ब में<ref name="Goldfarb.1981"/>हिल्बर्ट की 10वीं समस्या को दूसरे क्रम की एकीकरणीयता, समीकरण में घटाना <math>X_1 * X_2 = X_3</math> फलन चर के साथ चित्रित एकीकरण समस्या से मेल खाता है <math>F_i</math> तदनुसार <math>X_i</math> और <math>G</math> [[ताजा चर]].]]कई अनुप्रयोगों के लिए प्रथम-क्रम शब्दों के अतिरिक्त टाइप किए गए लैम्ब्डा-शब्दों के एकीकरण पर विचार करने की आवश्यकता होती है। इस प्रकार के एकीकरण को अधिकांशतः उच्च-क्रम एकीकरण कहा जाता है। उच्च-क्रम एकीकरण [[अनिर्णीत समस्या]] है,<ref name="Goldfarb.1981">{{cite journal| author=Warren D. Goldfarb| author-link=Warren D. Goldfarb| title=द्वितीय-क्रम एकीकरण समस्या की अनिर्णयता| journal=TCS| year=1981| volume=13| issue=2| pages=225–230| doi=10.1016/0304-3975(81)90040-2| doi-access=free}}</ref><ref>{{cite journal| author=Gérard P. Huet| title=तीसरे क्रम के तर्क में एकीकरण की अनिश्चितता| journal=Information and Control| year=1973| volume=22| issue=3| pages=257–267 |doi=10.1016/S0019-9958(73)90301-X| doi-access=free}}</ref><ref>Claudio Lucchesi: The Undecidability of the Unification Problem for Third Order Languages (Research Report CSRR 2059; Department of Computer Science, University of Waterloo, 1972)</ref> और ऐसी एकीकरण समस्याओं में अधिकांश सामान्य एकीकरणकर्ता नहीं होते हैं। उदाहरण के लिए, एकीकरण समस्या { f(a,b,a) ≐ d(b,a,c) }, जहां एकमात्र चर f है, में है
-सलूशन {f ↦ λx.λy.λz. d(y,x,c) }, {f ↦ λx.λy.λz. d(y,z,c) },
+हल {f ↦ λx.λy.λz. d(y,x,c) }, {f ↦ λx.λy.λz. d(y,z,c) },
 {f ↦ λx.λy.λz. d(y,a,c) }, {f ↦ λx.λy.λz. डी(बी,x,सी) },
-{f ↦ λx.λy.λz. d(b,z,c) } और {f ↦ λx.λy.λz. डी(बी,ए,सी) }. उच्च-क्रम यूनिफिकेशन की एक अच्छी प्रकार से अध्ययन की गई शाखा αβη रूपांतरणों द्वारा निर्धारित समानता को सरल रूप से टाइप किए गए लैम्ब्डा शब्दों मॉड्यूलो को एकीकृत करने की समस्या है। जेरार्ड ह्यूएट ने एक अर्ध-निर्णायक (पूर्व)यूनिफिकेशन कलनविधि दिया<ref>Gérard Huet: A Unification Algorithm for typed Lambda-Calculus []</ref> जो एकीकरणकर्ताओं के समष्टि की व्यवस्थित खोज की अनुमति देता है (मार्टेली-मोंटानारी के यूनिफिकेशन कलनविधि को सामान्यीकृत करना)<ref name="Martelli.Montanari.1982" />उच्च-क्रम वाले चर वाले शब्दों के नियमों के साथ) जो व्यवहार में पर्याप्त रूप से अच्छी प्रकार से काम करता प्रतीत होता है। Huet<ref>[http://portal.acm.org/citation.cfm?id=695200 Gérard Huet: Higher Order Unification 30 Years Later]</ref> और गाइल्स डोवेक<ref>Gilles Dowek: Higher-Order Unification and Matching. Handbook of Automated Reasoning 2001: 1009–1062</ref> इस विषय पर सर्वेक्षण करते हुए लेख लिखे हैं।
+{f ↦ λx.λy.λz. d(b,z,c) } और {f ↦ λx.λy.λz. डी(बी,ए,सी) }. उच्च-क्रम एकीकरण की एक अच्छी प्रकार से अध्ययन की गई शाखा αβη रूपांतरणों द्वारा निर्धारित समानता को सरल रूप से टाइप किए गए लैम्ब्डा शब्दों मॉड्यूलो को एकीकृत करने की समस्या है। जेरार्ड ह्यूएट ने एक अर्ध-निर्णायक (पूर्व) एकीकरण कलन विधि दिया<ref>Gérard Huet: A Unification Algorithm for typed Lambda-Calculus []</ref> जो एकीकरणकर्ताओं के समष्टि की व्यवस्थित खोज की अनुमति देता है (मार्टेली-मोंटानारी के एकीकरण कलन विधि को सामान्यीकृत करना)<ref name="Martelli.Montanari.1982" />उच्च-क्रम वाले चर वाले शब्दों के नियमों के साथ) जो व्यवहार में पर्याप्त रूप से अच्छी प्रकार से काम करता प्रतीत होता है। Huet<ref>[http://portal.acm.org/citation.cfm?id=695200 Gérard Huet: Higher Order Unification 30 Years Later]</ref> और गाइल्स डोवेक<ref>Gilles Dowek: Higher-Order Unification and Matching. Handbook of Automated Reasoning 2001: 1009–1062</ref> इस विषय पर सर्वेक्षण करते हुए लेख लिखे हैं।
-उच्च-क्रम यूनिफिकेशन के कई उपसमूह अच्छी प्रकार से व्यवहार किए जाते हैं, जिसमें वे निर्णय लेने योग्य होते हैं और हल करने योग्य समस्याओं के लिए सबसे सामान्य एकीकरणकर्ता होते हैं। ऐसा एक उपसमुच्चय पहले वर्णित प्रथम-क्रम पद है। डेल मिलर के कारण उच्च-क्रम पैटर्न एकीकरण,<ref>{{cite journal|first1=Dale|last1=Miller|title=लैम्ब्डा-एब्स्ट्रैक्शन, फंक्शन वेरिएबल्स और सरल एकीकरण के साथ एक लॉजिक प्रोग्रामिंग भाषा|journal=Journal of Logic and Computation|volume=1|issue=4|year=1991|pages=497–536|url=http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/jlc91.pdf|doi=10.1093/logcom/1.4.497}}</ref> ऐसा ही एक और उपसमुच्चय है। उच्च-क्रम लॉजिक प्रोग्रामिंग लैंग्वेजएं λप्रोलॉग और ट्वेल्फ़ पूर्ण उच्च-क्रम यूनिफिकेशन से मात्र पैटर्न खंड को लागू करने के लिए स्विच कर चुकी हैं; आश्चर्यजनक रूप से पैटर्न यूनिफिकेशन लगभग सभी कार्यक्रमों के लिए पर्याप्त है, यदि प्रत्येक गैर-पैटर्न यूनिफिकेशन समस्या को तब तक निलंबित कर दिया जाता है जब तक कि अगला प्रतिस्थापन यूनिफिकेशन को पैटर्न खंड में नहीं डाल देता। पैटर्न यूनिफिकेशन का एक सुपरसेट जिसे फलन -एज़-कंस्ट्रक्टर्स यूनिफिकेशन कहा जाता है, भी अच्छी प्रकार से व्यवहार किया जाता है।<ref>{{cite journal |last1=Libal |first1=Tomer |last2=Miller |first2=Dale |title=Functions-as-constructors higher-order unification: extended pattern unification |journal=Annals of Mathematics and Artificial Intelligence |date=May 2022 |volume=90 |issue=5 |pages=455–479 |doi=10.1007/s10472-021-09774-y|doi-access=free}}</ref> ज़िपरपोज़िशन प्रमेय कहावत में एक कलनविधि है जो इन अच्छे व्यवहार वाले उपसमुच्चय को पूर्ण उच्च-क्रम यूनिफिकेशन कलनविधि में एकीकृत करता है।<ref name="Vukmirovic">{{cite journal |last1=Vukmirović |first1=Petar |last2=Bentkamp |first2=Alexander |last3=Nummelin |first3=Visa |title=कुशल पूर्ण उच्च-क्रम एकीकरण|journal=Logical Methods in Computer Science |date=14 December 2021 |volume=17 |issue=4 |pages=6919 |doi=10.46298/lmcs-17(4:18)2021|doi-access=free }}</ref>
+उच्च-क्रम एकीकरण के कई उपसमूह अच्छी प्रकार से व्यवहार किए जाते हैं, जिसमें वे निर्णय लेने योग्य होते हैं और हल करने योग्य समस्याओं के लिए सबसे सामान्य एकीकरणकर्ता होते हैं। ऐसा एक उपसमुच्चय पहले वर्णित प्रथम-क्रम पद है। डेल मिलर के कारण उच्च-क्रम पैटर्न एकीकरण,<ref>{{cite journal|first1=Dale|last1=Miller|title=लैम्ब्डा-एब्स्ट्रैक्शन, फंक्शन वेरिएबल्स और सरल एकीकरण के साथ एक लॉजिक प्रोग्रामिंग भाषा|journal=Journal of Logic and Computation|volume=1|issue=4|year=1991|pages=497–536|url=http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/jlc91.pdf|doi=10.1093/logcom/1.4.497}}</ref> ऐसा ही एक और उपसमुच्चय है। उच्च-क्रम लॉजिक प्रोग्रामिंग लैंग्वेजएं λप्रोलॉग और ट्वेल्फ़ पूर्ण उच्च-क्रम एकीकरण से मात्र पैटर्न खंड को प्रयुक्त करने के लिए स्विच कर चुकी हैं; आश्चर्यजनक रूप से पैटर्न एकीकरण लगभग सभी कार्यक्रमों के लिए पर्याप्त है, यदि प्रत्येक गैर-पैटर्न एकीकरण समस्या को तब तक निलंबित कर दिया जाता है जब तक कि अगला प्रतिस्थापन एकीकरण को पैटर्न खंड में नहीं डाल देता। पैटर्न एकीकरण का एक सुपरसमुच्चय जिसे फलन -एज़-कंस्ट्रक्टर्स एकीकरण कहा जाता है, भी अच्छी प्रकार से व्यवहार किया जाता है।<ref>{{cite journal |last1=Libal |first1=Tomer |last2=Miller |first2=Dale |title=Functions-as-constructors higher-order unification: extended pattern unification |journal=Annals of Mathematics and Artificial Intelligence |date=May 2022 |volume=90 |issue=5 |pages=455–479 |doi=10.1007/s10472-021-09774-y|doi-access=free}}</ref> ज़िपरपोज़िशन प्रमेय कहावत में एक कलन विधि है जो इन अच्छे व्यवहार वाले उपसमुच्चय को पूर्ण उच्च-क्रम एकीकरण कलन विधि में एकीकृत करता है।<ref name="Vukmirovic">{{cite journal |last1=Vukmirović |first1=Petar |last2=Bentkamp |first2=Alexander |last3=Nummelin |first3=Visa |title=कुशल पूर्ण उच्च-क्रम एकीकरण|journal=Logical Methods in Computer Science |date=14 December 2021 |volume=17 |issue=4 |pages=6919 |doi=10.46298/lmcs-17(4:18)2021|doi-access=free }}</ref>
-अभिकलनात्मक लैंग्वेज विज्ञान में [[अण्डाकार निर्माण]] के सबसे प्रभावशाली सिद्धांतों में से एक यह है कि दीर्घवृत्त को मुक्त चर द्वारा दर्शाया जाता है, जिनके मान तब उच्च-क्रम यूनिफिकेशन का उपयोग करके निर्धारित किए जाते हैं। उदाहरण के लिए जॉन का अर्थपूर्ण प्रतिनिधित्व मैरी को पसंद है और पीटर को भी पसंद है {{math| like(''j'', ''m'') &and; R(''p'') }} और आर का मान (दीर्घवृत्त का अर्थपूर्ण प्रतिनिधित्व) समीकरण द्वारा निर्धारित किया जाता है {{math| like(''j'', ''m'') {{=}} R(''j'')  }}. ऐसे समीकरणों को हल करने की प्रक्रिया को उच्च-क्रम यूनिफिकेशन कहा जाता है।<ref>{{cite book| first1 = Claire | last1 = Gardent |author1-link=Claire Gardent| first2 = Michael | last2 = Kohlhase | first3 = Karsten | last3 = Konrad | author2-link=Michael Kohlhase| chapter=A Multi-Level, Higher-Order Unification Approach to Ellipsis| title=Submitted to European [[Association for Computational Linguistics]] (EACL)<!---according to http://page.mi.fu-berlin.de/cbenzmueller/papers/R8.pdf--->| year=1997|citeseerx = 10.1.1.55.9018}}</ref>
+अभिकलनात्मक लैंग्वेज विज्ञान में [[अण्डाकार निर्माण]] के सबसे प्रभावशाली सिद्धांतों में से एक यह है कि दीर्घवृत्त को मुक्त चर द्वारा दर्शाया जाता है, जिनके मान तब उच्च-क्रम एकीकरण का उपयोग करके निर्धारित किए जाते हैं। उदाहरण के लिए जॉन का अर्थपूर्ण प्रतिनिधित्व मैरी को पसंद है और पीटर को भी पसंद है {{math| like(''j'', ''m'') &and; R(''p'') }} और आर का मान (दीर्घवृत्त का अर्थपूर्ण प्रतिनिधित्व) समीकरण द्वारा निर्धारित किया जाता है {{math| like(''j'', ''m'') {{=}} R(''j'')  }}. ऐसे समीकरणों को हल करने की प्रक्रिया को उच्च-क्रम एकीकरण कहा जाता है।<ref>{{cite book| first1 = Claire | last1 = Gardent |author1-link=Claire Gardent| first2 = Michael | last2 = Kohlhase | first3 = Karsten | last3 = Konrad | author2-link=Michael Kohlhase| chapter=A Multi-Level, Higher-Order Unification Approach to Ellipsis| title=Submitted to European [[Association for Computational Linguistics]] (EACL)<!---according to http://page.mi.fu-berlin.de/cbenzmueller/papers/R8.pdf--->| year=1997|citeseerx = 10.1.1.55.9018}}</ref>
-[[वेन स्नाइडर]] ने उच्च-क्रम यूनिफिकेशन और ई-यूनिफिकेशन दोनों का सामान्यीकरण दिया, अर्थात लैम्ब्डा-शब्द मॉड्यूलो को एक समीकरण सिद्धांत को एकीकृत करने के लिए एक एल्गोरिदम।<ref>{{cite book | author=Wayne Snyder | contribution=Higher order E-unification | title=प्रोक. स्वचालित कटौती पर 10वां सम्मेलन| publisher=Springer | series=LNAI | volume=449 | pages=573–587 |date=Jul 1990 | title-link=Conference on Automated Deduction }}</ref>
+[[वेन स्नाइडर]] ने उच्च-क्रम एकीकरण और ई- एकीकरण दोनों का सामान्यीकरण दिया, अर्थात लैम्ब्डा-शब्द मॉड्यूलो को एक समीकरण सिद्धांत को एकीकृत करने के लिए एक एल्गोरिदम।<ref>{{cite book | author=Wayne Snyder | contribution=Higher order E-unification | title=प्रोक. स्वचालित कटौती पर 10वां सम्मेलन| publisher=Springer | series=LNAI | volume=449 | pages=573–587 |date=Jul 1990 | title-link=Conference on Automated Deduction }}</ref>
@@ Line 648: / Line 655: @@
 *[[लैम्ब्डा कैलकुलस]] में [[स्पष्ट प्रतिस्थापन]]
 *गणितीय [[समीकरण हल करना]]
-*डिस-यूनिफिकेशन (कंप्यूटर विज्ञान)|डिस-यूनिफिकेशन: सिंबॉलिक एक्सप्रेशन के बीच असमानताओं को हल करना
+*डिस- एकीकरण (कंप्यूटर विज्ञान)|डिस-यूनिफिकेशन: सिंबॉलिक अभिव्यक्तियों के बीच असमानताओं को हल करना
-*एंटी-यूनिफिकेशन (कंप्यूटर साइंस)|एंटी-यूनिफिकेशन: दो शब्दों के कम से कम सामान्य सामान्यीकरण (एलजीजी) की गणना करना, सबसे सामान्य उदाहरण (एमजीयू) की गणना करना
+*एंटी- एकीकरण (कंप्यूटर साइंस)|एंटी-यूनिफिकेशन: दो शब्दों के कम से कम सामान्य सामान्यीकरण (एलजीजी) की गणना करना, सबसे सामान्य उदाहरण (एमजीयू) की गणना करना
-*सब्समिशन जाली, एक जाली जिसमें मिलन के रूप में यूनिफिकेशन और जुड़ने के रूप में विरोधी यूनिफिकेशन होता है
+*सब्समिशन जाली, एक जाली जिसमें मिलन के रूप में एकीकरण और जुड़ने के रूप में विरोधी एकीकरण होता है
-*ओन्टोलॉजी संरेखण ([[शब्दार्थ तुल्यता]] के साथ यूनिफिकेशन का उपयोग करें)
+*ओन्टोलॉजी संरेखण ([[शब्दार्थ तुल्यता]] के साथ एकीकरण का उपयोग करें)
 ==टिप्पणियाँ==
@@ Line 673: / Line 680: @@
 * {{cite journal | last1 = Raulefs | first1 = Peter | last2 = Siekmann | first2 = Jörg | last3 = Szabó | first3 = P. | last4 = Unvericht | first4 = E. | year = 1979 | title = A short survey on the state of the art in matching and unification problems | journal = ACM SIGSAM Bulletin | volume = 13 | issue = 2 | pages = 14–20 | doi = 10.1145/1089208.1089210 | s2cid = 17033087 }}
 * Claude Kirchner and Hélène Kirchner. ''Rewriting, Solving, Proving''. In preparation.
-[[Category: एकीकरण (कंप्यूटर विज्ञान)| एकीकरण]] [[Category: स्वचालित प्रमेय सिद्ध करना]] [[Category: तर्क प्रोग्रामिंग]] [[Category: पुनर्लेखन प्रणाली]] [[Category: कंप्यूटर विज्ञान में तर्क]] [[Category: प्रकार सिद्धांत]]
-[[Category: Machine Translated Page]]
+[[Category:All articles with dead external links]]
+[[Category:Articles using small message boxes]]
+[[Category:Articles with dead external links from March 2021]]
+[[Category:Articles with hatnote templates targeting a nonexistent page]]
+[[Category:Articles with permanently dead external links]]
+[[Category:CS1]]
+[[Category:CS1 maint]]
 [[Category:Created On 14/07/2023]]
+[[Category:Machine Translated Page]]
+[[Category:Pages with script errors]]
+[[Category:Templates Vigyan Ready]]
+[[Category:Webarchive template wayback links]]
+[[Category:एकीकरण (कंप्यूटर विज्ञान)| एकीकरण]]
+[[Category:कंप्यूटर विज्ञान में तर्क]]
+[[Category:तर्क प्रोग्रामिंग]]
+[[Category:पुनर्लेखन प्रणाली]]
+[[Category:प्रकार सिद्धांत]]
+[[Category:स्वचालित प्रमेय सिद्ध करना]]

Anonymous

Search

एकीकरण (कंप्यूटर विज्ञान): Difference between revisions

Latest revision as of 11:05, 12 August 2023

फॉर्मल परिभाषा

प्रिरेक्विज़िट

प्रतिस्थापन

सामान्यीकरण, विशेषज्ञता

हल समुच्चय

प्रथम-क्रम शब्दों का वाक्यात्मकएकीकरण

एक एकीकरण कलन विधि

ओक्कुर चेक

समाप्ति का प्रमाण

प्रथम-क्रम शब्दों के वाक्यात्मकएकीकरण के उदाहरण

अनुप्रयोग: लॉजिक प्रोग्रामिंग में एकीकरण

अनुप्रयोग: प्रकार अनुमान

अनुप्रयोग: फ़ीचर संरचना एकीकरण

क्रमानुसार एकीकरण

अनंत पदों का एकीकरण

ई-एकीकरण

विशेष पृष्ठभूमि ज्ञान समुच्चय E

एकतरफा पैरामोड्यूलेशन

संकुचन

उच्च-क्रम एकीकरण

यह भी देखें

टिप्पणियाँ

संदर्भ

अग्रिम पठन

Navigation

Wiki tools

Page tools

Other projects

Categories