एकीकरण (कंप्यूटर विज्ञान): 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> के रूप में होता हैं। समीकरण समुच्चय या एकीकरण समस्या में किन अभिव्यक्तियों या शब्दों को घटित होने की अनुमति होती है और किन अभिव्यक्तियों को समान माना जाता है, इसके आधार पर एकीकरण के रूप में कई ढांचे प्रतिष्ठित हैं। यदि उच्च-क्रम वाले चर अर्थात [[फ़ंक्शन (गणित)|फलन (गणित)]] का प्रतिनिधित्व करने वाले चर को एक अभिव्यक्तियों में अनुमति होती है, तो प्रक्रिया को 'उच्च-क्रम एकीकरण' कहा जाता है। अन्यथा 'प्रथम-क्रम एकीकरण' का रूप कहा जाता है। यदि प्रत्येक समीकरण के दोनों पक्षों को वस्तुतः समान बनाने के लिए किसी समाधान की आवश्यकता होती है, तो प्रक्रिया को 'वाक्यविन्यास' या 'मुक्त एकीकरण' कहा जाता है, अन्यथा सिमेंटिक या 'समीकरणात्मक एकीकरण या ई- एकीकरण या एकीकरण मॉड्यूलो सिद्धांत कहा जाता है।
+=== '''प्रिरेक्विज़िट''' ===
+औपचारिक रूप से एक एकीकरण दृष्टिकोण का अनुमान लगाया जाता है
+* एक अनंत समुच्चय <math>V</math> चर का. उच्च-क्रम एकीकरण के लिए, इसे चुनना सुविधाजनक है <math>V</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>\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> अल्फ़ा समतुल्य होता है.
-यदि प्रत्येक समीकरण का दाहिना भाग बंद है (कोई मुक्त चर नहीं है), तो समस्या को (पैटर्न) मिलान कहा जाता है। प्रत्येक समीकरण के बाईं ओर (चर के साथ) को पैटर्न कहा जाता है।<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>
+शब्दों और सिद्धांत का समुच्चय समाधानों के समुच्चय को कैसे प्रभावित करता है, इसके उदाहरण के रूप में वाक्यात्मक प्रथम-क्रम एकीकरण समस्या { 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 ↦ को किसी भी मान पर मैप करता है।
-===आवश्यकताएँ===
+==='''प्रतिस्थापन'''===
-औपचारिक रूप से, एक एकीकरण दृष्टिकोण का अनुमान लगाया जाता है
+{{main|प्रतिस्थापन (लॉजिक)}}
-* एक अनंत समुच्चय <math>V</math> चर का. उच्च-क्रम एकीकरण के लिए, इसे चुनना सुविधाजनक है <math>V</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>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>\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 } एक [[अर्धसमूह]] में समाधान के रूप में होता है, अर्थात यदि (⋅) को साहचर्य माना जाता है . लेकिन वही समस्या, जिसे [[एबेलियन समूह]] में देखा जाता है, जहां (⋅) को क्रम[[विनिमेय]] भी माना जाता है, समाधान के रूप में कोई भी प्रतिस्थापन होता है।
-उच्च-क्रम एकीकरण के उदाहरण के रूप में, एकल सेट { a = y(x) } एक वाक्यात्मक दूसरे क्रम की एकीकरण समस्या है, क्योंकि y एक फ़ंक्शन चर है। एक समाधान है {x ↦ a, y ↦ (पहचान फलन) }; दूसरा है { y ↦ (निरंतर फ़ंक्शन प्रत्येक मान को a पर मैप करता है), x ↦ (कोई भी मान) }।
-===प्रतिस्थापन===
-{{main|Substitution (logic)}}
-प्रतिस्थापन एक मानचित्रण है <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|{{mset| ''x'' ↦ ''h''(''a'',''y''), ''z'' ↦ ''b'' }}}}शब्द के लिए
- {|
 |-
 |
@@ Line 37: / Line 29: @@
 | <math> ), y)</math>
 |-
-| yields &nbsp;
+| प्रतिफल
 |-
 |
@@ Line 47: / Line 39: @@
 |}
+==='''सामान्यीकरण, विशेषज्ञता'''===
+यदि एक शब्द <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>.गुणधर्म है
-===सामान्यीकरण, विशेषज्ञता===
+यदि ≡ शब्दों की शाब्दिक वाक्यविन्यास के रूप में पहचान है, तो एक शब्द दूसरे की तुलना में अधिक सामान्य और अधिक विशेष दोनों हो सकते है, यदि दोनों शब्द मात्र उनके परिवर्तनीय नामों में भिन्न हों न कि उनकी वाक्यात्मक संरचना में ऐसे शब्दों को परिवर्त या एक-दूसरे का नाम बदलना कहा जाता है।
-यदि एक शब्द <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>f(x_1, a, g(z_1), y_1)</math>
-का एक प्रकार है
+का एक प्रकार होता है
   <math>f(x_2, a, g(z_2), y_2)</math>,
-तब से
+जब से
 <math display="block">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) </math>
 और
 <math display="block">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).</math>
-चूंकि, <math>f(x_1, a, g(z_1), y_1)</math> का एक प्रकार नहीं है  <math>f(x_2, a, g(x_2), x_2)</math>, क्योंकि कोई भी प्रतिस्थापन पश्चात वाले पद को पहले वाले में नहीं बदल सकता।
+चूंकि, <math>f(x_1, a, g(z_1), y_1)</math> का एक प्रकार नहीं है <math>f(x_2, a, g(x_2), x_2)</math>, क्योंकि कोई भी प्रतिस्थापन पश्चात वाले पद को पहले वाले में नहीं बदल सकता है।
-इसलिए पश्चात वाला शब्द पहले वाले की तुलना में उचित रूप से अधिक विशेष है।
-मनमानी के लिए <math>\equiv</math>, एक शब्द संरचनात्मक रूप से भिन्न शब्द की तुलना में अधिक सामान्य और अधिक विशेष दोनों हो सकता है।
+इसलिए पश्चात वाला शब्द पहले वाले की तुलना में उचित रूप से अधिक विशेष होता है।
-उदाहरण के लिए, यदि ⊕ [[निष्क्रिय]] है, अर्थात यदि सदैव <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> सहायक चर जैसे कि कोई समीकरण नहीं <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>\equiv</math>, एक शब्द संरचनात्मक रूप से भिन्न शब्द की तुलना में अधिक सामान्य और अधिक विशेष दोनों हो सकता है।
+उदाहरण के लिए, यदि ⊕ [[निष्क्रिय]] है, अर्थात यदि सदैव <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 = \{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>}}</ref>
+<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 का एकीकरण कर्ता भी कहा जाता है।
-===समाधान सेट===
+उदाहरण के लिए, यदि ⊕ साहचर्य है, तो एकीकरण समस्या {''x'' ⊕ ''a'' ≐ ''a'' ⊕ ''x'' } के हल हैं {''x'' ↦ ''a' '}, {''x'' ↦ ''a'' ⊕ ''a''}, {''x'' ↦ ''a'' ⊕ ''a'' ⊕ ''a''}, आदि ,जबकि समस्या { ''x'' ⊕ ''a'' ≐ ''a'' } का कोई हल नहीं होता है।''
-एक प्रतिस्थापन σ एकीकरण समस्या ''ई'' का एक समाधान है यदि {{math|''l''<sub>''i''</sub>σ ≡ ''r''<sub>''i''</sub>σ}} के लिए <math>i = 1, ..., n</math>. ऐसे प्रतिस्थापन को ''ई'' का एकीकरणकर्ता भी कहा जाता है।
+दी गई एकीकरण समस्या E के लिए, एकीकरण कर्ताओं के एक समुच्चय ''S'' को पूर्ण कहा जाता है यदि प्रत्येक हल प्रतिस्थापन को ''एस'' में कुछ प्रतिस्थापन द्वारा समाहित किया जाता है। एक पूर्ण प्रतिस्थापन समुच्चय निरंतर उपलब्ध होता है, उदाहरण के लिए सभी समाधानों का समुच्चय लेकिन कुछ रूप रेखाओं में जैसे कि अप्रतिबंधित उच्च-क्रम एकीकरण में यह निर्धारित करने की समस्या होती है, कि क्या पूर्ण प्रतिस्थापन समुच्चय गैर रिक्त अनिर्णीत रूप में होता है।
-उदाहरण के लिए, यदि ⊕ साहचर्य है, तो एकीकरण समस्या {''x'' ⊕ ''a'' ≐ ''a'' ⊕ ''x'' } के समाधान हैं {''x'' ↦ ''a' '}, {''x'' ↦ ''a'' ⊕ ''a''}, {''x'' ↦ ''a'' ⊕ ''a'' ⊕ ''a''}, आदि ., जबकि समस्या { ''x'' ⊕ ''a'' ≐ ''a'' } का कोई समाधान नहीं है।
-दी गई एकीकरण समस्या ''ई'' के लिए, एकीकरणकर्ताओं के एक सेट ''एस'' को पूर्ण कहा जाता है यदि प्रत्येक समाधान प्रतिस्थापन को ''एस'' में कुछ प्रतिस्थापन द्वारा समाहित किया जाता है। एक पूर्ण प्रतिस्थापन सेट निरंतर उपलब्ध होता है (उदाहरण के लिए सभी समाधानों का सेट), लेकिन कुछ रूपरेखाओं में (जैसे कि अप्रतिबंधित उच्च-क्रम एकीकरण) यह निर्धारित करने की समस्या कि क्या कोई समाधान उपलब्ध है (अर्थात, क्या पूर्ण प्रतिस्थापन सेट गैर-रिक्त है) अनिर्णीत है।
+समुच्चय ''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|प्रतिस्थापन σ द्वारा टर्म t1 और t2 को वाक्यात्मकरूप से एकीकृत करने का योजनाबद्ध त्रिभुज आरेख है]]प्रथम-क्रम शब्दों का वाक्यात्मक एकीकरण सबसे व्यापक रूप से उपयोग किया जाने वाला एकीकरण ढांचा है।
+यह प्रथम-क्रम के पदों के समुच्चय 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|''σ''}}}}.
-[[File:Triangle diagram of syntactic unification svg.svg|thumb|वाक्यविन्यास की दृष्टि से एकीकृत शब्दों का योजनाबद्ध त्रिभुज आरेख टी<sub>1</sub> और टी<sub>2</sub> एक प्रतिस्थापन द्वारा पी]]प्रथम-क्रम शब्दों का वाक्यात्मक एकीकरण सबसे व्यापक रूप से उपयोग किया जाने वाला एकीकरण ढांचा है।
-यह प्रथम-क्रम के पदों के समुच्चय T पर आधारित है (चरों के कुछ दिए गए समुच्चय V, स्थिरांकों के C और F पर)<sub>''n''</sub> n-ary फ़ंक्शन प्रतीकों का) और ≡ वाक्यगत समानता पर है।
+इसके सदस्य {{mvar|σ}} को समस्या का सबसे सामान्य एकीकरणकर्ता (एमजीयू) का रूप कहा जाता है।
-इस ढांचे में, प्रत्येक समाधान योग्य एकीकरण समस्या {{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|σ}}.
+समस्या का कोई भी एकीकरणकर्ता समाहित हो जाता है<ref group="note">formally: each unifier τ satisfies {{math|1=∀''x'': ''xτ'' = (''xσ'')''ρ''}} for some substitution ρ</ref> एमजीयू द्वारा {{mvar|σ}}.
-एमजीयू वेरिएंट तक अद्वितीय है: यदि एस<sub>1</sub> और एस<sub>2</sub> दोनों एक ही वाक्यात्मक एकीकरण समस्या के पूर्ण और न्यूनतम समाधान सेट हैं, तो एस<sub>1</sub> = {पी<sub>1</sub> } और एस<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) }, क्योंकि
@@ Line 109: / Line 109: @@
 | .
 |}
-यह सबसे सामान्य एकीकरणकर्ता भी है।
+यह सबसे सामान्य एकीकरणकर्ता के रूप में है
-समान समस्या के लिए अन्य एकीकरणकर्ता हैं, उदा. { एक्स ↦ एफ(एक्स<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 142: / Line 143: @@
 {{hidden end}}
 }}
-रॉबिन्सन (1965) द्वारा दिया गया पहला एल्गोरिदम अधिक अप्रभावी था; सी एफ डिब्बा।
+रॉबिन्सन (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>
-यह पेपर एक कुशल वाक्यात्मक एकीकरण एल्गोरिदम खोजने के पिछले प्रयासों को भी सूचीबद्ध करता है,<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}}
+निम्नलिखित तेज़ कलन विधि की उत्पत्ति मार्टेली, मोंटानारी (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}} का रूप होता है.
+एक परिमित समुच्चय दिया गया है <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>.
+इस फॉर्म के एक समुच्चय को प्रतिस्थापन के रूप में पढ़ा जा सकता है।
+यदि कोई हल नहीं है, तो कलन विधि ⊥ के साथ समाप्त हो जाता है; अन्य लेखक Ω , {} के रूप में उपयोग करते हैं या उस स्थिति में विफल हो जाते हैं।
-एक परिमित समुच्चय दिया गया है <math>G = \{ s_1 \doteq t_1, ..., s_n \doteq t_n \}</math> संभावित समीकरणों का,
-एल्गोरिथ्म इसे फॉर्म के समीकरणों के समतुल्य सेट में बदलने के लिए नियम लागू करता है
-{ एक्स<sub>1</sub> ≐ यू<sub>1</sub>, ..., एक्स<sub>''m''</sub> ≐ यू<sub>''m''</sub> }
-कहां एक्स<sub>1</sub>, ..., एक्स<sub>''m''</sub> भिन्न-भिन्न चर हैं और यू<sub>1</sub>, ..., में<sub>''m''</sub> ऐसे पद हैं जिनमें x में से कोई भी नहीं है<sub>''i''</sub>.
-इस फॉर्म के एक सेट को प्रतिस्थापन के रूप में पढ़ा जा सकता है।
-यदि कोई समाधान नहीं है तो एल्गोरिथ्म ⊥ के साथ समाप्त हो जाता है; अन्य लेखक Ω , {} का उपयोग करते हैं, या उस स्थिति में विफल हो जाते हैं।
 समस्या G में चर x की सभी घटनाओं को पद t से प्रतिस्थापित करने की क्रिया को G {x ↦ t} दर्शाया गया है।
-सरलता के लिए, स्थिर प्रतीकों को शून्य तर्क वाले फ़ंक्शन प्रतीकों के रूप में माना जाता है।
+सरलता के लिए, स्थिर प्रतीकों को शून्य लॉजिक वाले फलन प्रतीकों के रूप में माना जाता है।
 :{|
@@ Line 194: / Line 204: @@
-====चेक होता है====
+===='''ओक्कुर चेक''' ====
-{{main|Occurs check}}
+{{main|ओक्कुर चेक}}
-एक चर x को एक ऐसे पद के साथ एकीकृत करने का प्रयास जिसमें x एक सख्त उपपद x ≐ f(..., x, ...) के रूप में हो, x के समाधान के रूप में एक अनंत पद की ओर ले जाएगा, क्योंकि x स्वयं के एक उपपद के रूप में घटित होगा .
-जैसा कि ऊपर परिभाषित किया गया है (परिमित) प्रथम-क्रम शब्दों के सेट में, समीकरण x ≐ f(..., x, ...) का कोई समाधान नहीं है; इसलिए उन्मूलन नियम मात्र तभी लागू किया जा सकता है यदि x ∉ vars(t)।
-चूँकि वह अतिरिक्त जाँच, जिसे 'चेक होता है' कहा जाता है, एल्गोरिथम को धीमा कर देती है, इसलिए इसे छोड़ दिया जाता है, उदाहरण के लिए अधिकांश प्रोलॉग सिस्टम में।
-सैद्धांतिक दृष्टिकोण से, चेक को छोड़ना अनंत पेड़ों पर समीकरणों को हल करने के समतुल्य है, नीचे अनंत पदों का #एकीकरण देखें।
-====समाप्ति का प्रमाण====
+एक चर x को एक ऐसे पद के साथ एकीकृत करने का प्रयास जिसमें x एक सख्त उपपद x ≐ f(..., x, ...) के रूप में हो, x के हल के रूप में एक अनंत पद की ओर ले जाता है, क्योंकि x स्वयं के एक उपपद के रूप में घटित होता है
-एल्गोरिथम की समाप्ति के प्रमाण के लिए ट्रिपल पर विचार करें <math>\langle n_{var}, n_{lhs}, n_{eqn}\rangle</math>
-कहाँ {{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>}} दोबारा।
-जब नियम विघटित, संघर्ष, या अदला-बदली लागू किया जाता है, {{math|''n''<sub>''lhs''</sub>}} कम हो जाता है, क्योंकि कम से कम बायीं ओर का सबसे बाहरी एफ गायब हो जाता है।
-बाकी किसी भी नियम को लागू करने से डिलीट या चेक नहीं बढ़ सकेगा {{math|''n''<sub>''lhs''</sub>}}, लेकिन घट जाती है {{math|''n''<sub>''eqn''</sub>}}.
-इसलिए, किसी भी नियम को लागू करने से तीन गुना कम हो जाता है <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> [[एपिग्राम (प्रोग्रामिंग भाषा)]] जैसी आश्रित रूप से टाइप की गई भाषा में एकीकरण जिस संरचना का उपयोग करता है, उसे व्यक्त करके, रॉबिन्सन के एकीकरण एल्गोरिदम को चर की संख्या पर पुनरावर्ती बनाया जा सकता है, जिस स्थिति में एक भिन्न समाप्ति प्रमाण अनावश्यक हो जाता है।
+जैसा कि ऊपर परिभाषित किया गया है (परिमित) प्रथम-क्रम शब्दों के समुच्चय में समीकरण x ≐ f(..., x, ...) का कोई हल नहीं है; इसलिए उन्मूलन नियम मात्र तभी प्रयुक्त किया जा सकता है यदि x ∉ वार्स(t)।
-===प्रथम-क्रम शब्दों के वाक्यात्मक एकीकरण के उदाहरण===
+चूँकि वह अतिरिक्त जाँच जिसे 'एक्सेस चेक' कहा जाता है, कलन विधि को धीमा कर देती है, इसलिए इसे छोड़ दिया जाता है, उदाहरण के लिए अधिकांश प्रोलॉग प्रणाली में होता है।
-प्रोलॉग सिंटैक्टिकल कन्वेंशन में अपरकेस अक्षर से प्रारंभ होने वाला प्रतीक एक परिवर्तनीय नाम है; एक प्रतीक जो छोटे अक्षर से प्रारंभ होता है वह एक फ़ंक्शन प्रतीक है; अल्पविराम का उपयोग तार्किक और ऑपरेटर के रूप में किया जाता है।
-गणितीय संकेतन के लिए, x,y,z को चर के रूप में, f,g को फ़ंक्शन प्रतीकों के रूप में, और a,b को स्थिरांक के रूप में उपयोग किया जाता है।
+सैद्धांतिक दृष्टिकोण से, चेक को छोड़ना अनंत पेड़ों पर समीकरणों को हल करने के समतुल्य है, नीचे अनंत पदों का # एकीकरण के रूप में देख़ते है।
+===='''समाप्ति का प्रमाण'''====
+कलन विधि की समाप्ति के प्रमाण के लिए ट्रिपल पर विचार करें <math>\langle n_{var}, n_{lhs}, n_{eqn}\rangle</math>
+जहाँ {{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>}} दोबारा होता है ।
+जब नियम विघटित, संघर्ष, या अदला-बदली प्रयुक्त के रूप में किया जाता है, {{math|''n''<sub>''lhs''</sub>}} कम हो जाता है, क्योंकि कम से कम बायीं ओर का सबसे बाहरी f गायब हो जाता है।
+बाकी किसी भी नियम को प्रयुक्त करने से डिलीट या चेक नहीं बढ़ सकेगा {{math|''n''<sub>''lhs''</sub>}}, लेकिन घट जाती है {{math|''n''<sub>''eqn''</sub>}}.
+इसलिए किसी भी नियम को प्रयुक्त करने से तीन गुना कम हो जाता है <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> [[एपिग्राम (प्रोग्रामिंग भाषा)|एपिग्राम (प्रोग्रामिंग लैंग्वेज)]] जैसी आश्रित रूप से टाइप की गई लैंग्वेज में एकीकरण जिस संरचना का उपयोग करता है, उसे व्यक्त करके रॉबिन्सन के एकीकरण कलन विधि को चर की संख्या पर पुनरावर्ती बनाया जा सकता है, जिस स्थिति में एक भिन्न समाप्ति प्रमाण अनावश्यक हो जाता है।
+==='''प्रथम-क्रम शब्दों के वाक्यात्मकएकीकरण के उदाहरण'''===
+प्रोलॉग सिंटैक्टिकल कन्वेंशन में अपर केस अक्षर से प्रारंभ होने वाला प्रतीक एक परिवर्तनीय नाम है; एक प्रतीक जो छोटे अक्षर से प्रारंभ होता है. वह एक फलन प्रतीक है, अल्पविराम का उपयोग तार्किक और ऑपरेटर के रूप में किया जाता है।
+गणितीय संकेतन के लिए, x,y,z को चर के रूप में, f,g को फलन प्रतीकों के रूप में, और a,b को स्थिरांक के रूप में उपयोग किया जाता है।
 {| class="wikitable"
 |-
-! Prolog notation !! Mathematical notation !! Unifying substitution !! Explanation
+! प्रकल संकेतन !! गणितीय संकेतन !! एकताकारी प्रतिस्थापन !! निरूपण
 |-
-| <code> a = a </code> || { ''a'' = ''a'' } ||  {}  || Succeeds. ([[Tautology (logic)|tautology]])
+| <code> a = a </code> || { ''a'' = ''a'' } ||  {}  || सक्सीड (टॉटोलॉजी)
 |-
-| <code> a = b </code> || { ''a'' = ''b'' }  || ⊥ || ''a'' and ''b'' do not match
+| <code> a = b </code> || { ''a'' = ''b'' }  || ⊥ || a और b मेल नहीं खाते
 |-
-| <code> X = X </code> || { ''x'' = ''x'' } || {} || Succeeds. ([[Tautology (logic)|tautology]])
+| <code> X = X </code> || { ''x'' = ''x'' } || {} || सक्सीड (टॉटोलॉजी)
 |-
-| <code> a = X </code> || { ''a'' = ''x'' }  || { ''x'' ↦ ''a'' } || ''x'' is unified with the constant ''a''
+| <code> a = X </code> || { ''a'' = ''x'' }  || { ''x'' ↦ ''a'' } || ''x'' स्थिरांक के साथ एकीकृत है ''a''
 |-
-| <code> X = Y </code> || { ''x'' = ''y'' }  || { ''x'' ↦ ''y'' } || ''x'' and ''y'' are aliased
+| <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'' } || function and constant symbols match, ''x'' is unified with the constant ''b''
+| <code> f(a,X) = f(a,b) </code> || { ''f''(''a'',''x'') = ''f''(''a'',''b'') } ||  { ''x'' ↦ ''b'' } || फलन और स्थिरांक प्रतीक मेल खाते हैं, x स्थिरांक b के साथ एकीकृत है
 |-
-| <code> f(a) = g(a) </code> || { ''f''(''a'') = ''g''(''a'') }  || ⊥ || ''f'' and ''g'' do not match
+| <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'' and ''y'' are aliased
+| <code> f(X) = f(Y) </code> || { ''f''(''x'') = ''f''(''y'') } || { ''x'' ↦ ''y'' } || x और y अलियास हैं
 |-
-| <code> f(X) = g(Y) </code> || { ''f''(''x'') = ''g''(''y'') } || ⊥ || ''f'' and ''g'' do not match
+| <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'') } || ⊥ || Fails. The ''f'' function symbols have different arity
+| <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'') } || Unifies ''y'' with the term {{tmath|g(x)}}
+| <code> f(g(X)) = f(Y) </code> || { ''f''(''g''(''x'')) = ''f''(''y'') } || { ''y'' ↦ ''g''(''x'') } || y को पद के साथ एकीकृत करता है {{tmath|g(x)}}
 |-
-| <code> f(g(X),X) = f(Y,a) </code> || { ''f''(''g''(''x''),''x'') = ''f''(''y'',''a'') } || { ''x'' ↦ ''a'', ''y'' ↦ ''g''(''a'') } || Unifies ''x'' with constant ''a'', and ''y'' with the term {{tmath|g(a)}}
+| <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 ⊥ || Returns ⊥ in first-order logic and many modern Prolog dialects (enforced by the ''[[occurs check]]'').
+| <code> X = f(X) </code> || { ''x'' = ''f''(''x'') } || should be ⊥ || प्रथम-क्रम लॉजिक और कई आधुनिक प्रोलॉग बोलियों में रिटर्न ⊥ ओक्कुर चेक [[चेक द्वारा लागू|द्वारा प्रयुक्त]] होता है।
-Succeeds in traditional Prolog and in Prolog II, unifying ''x'' with infinite term <code>x=f(f(f(f(...))))</code>.
+पारंपरिक प्रोलॉग और प्रोलॉग 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'' } || Both ''x'' and ''y'' are unified with the constant ''a''
+| <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'' } || As above (order of equations in set doesn't matter)
+| <code> a = Y, X = Y </code> || { ''a'' = ''y'', ''x'' = ''y'' } || { ''x'' ↦ ''a'', ''y'' ↦ ''a'' } || जैसा कि ऊपर बताया गया है (समुच्चय में समीकरणों का क्रम मायने नहीं रखता हैं)
 |-
-| <code> X = a, b = X </code> || { ''x'' = ''a'', ''b'' = ''x'' }  || ⊥ || Fails. ''a'' and ''b'' do not match, so ''x'' can't be unified with both
+| <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)) \} }}, सीएफ. चित्र। इस प्रकार के विस्फोट के कारण होने वाली घातीय समय सम्मिश्रता से बचने के लिए, उन्नत एकीकरण एल्गोरिदम पेड़ों  के अतिरिक्त निर्देशित एसाइक्लिक आलेख़ (डैग) पर काम करते हैं।{{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>True : ['x', 'y', 'z']</code> सही ढंग से टाइप नहीं किया गया है. सूची निर्माण फ़ंक्शन <code>(:)</code> प्रकार का है <code>a -> [a] -> [a]</code>, और पहले तर्क के लिए <code>True</code> बहुरूपी प्रकार चर <code>a</code> के साथ एकाकार होना होगा <code>True</code>का प्रकार, <code>Bool</code>. दूसरा तर्क, <code>['x', 'y', 'z']</code>, प्रकार का है <code>[Char]</code>, लेकिन <code>a</code> दोनों नहीं हो सकते <code>Bool</code> और <code>Char</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>
+=='''क्रमानुसार एकीकरण'''==
+[[क्रमबद्ध तर्क|क्रमबद्ध लॉजिक]] प्रत्येक पद के लिए एक सॉर्ट या प्रकार निर्दिष्ट करने और एक सॉर्ट s1 घोषित करने की अनुमति देता है, दूसरे प्रकार का एक उपवर्ग s<sub>2</sub>, घोषित करने की अनुमति देता है, जिसे आमतौर पर s1 ⊆ s2 के रूप में लिखा जाता है। उदाहरण के लिए जैविक प्राणियों के बारे में लॉजिक करते समय एक प्रकार के कुत्ते को एक प्रकार के जानवर का उपवर्ग के रूप में घोषित करना उपयोगी होता है। जहां भी किसी प्रकार के शब्द की आवश्यकता होती है, उसके समष्टि पर किसी भी प्रकार के शब्द की आपूर्ति की जा सकती है।
-==क्रमानुसार एकीकरण==
+उदाहरण के लिए एक फलन घोषणा मां: जानवर → जानवर, और एक निरंतर घोषणा लस्सी: कुत्ता मानते हुए, मां (लस्सी) शब्द पूरी प्रकार से मान्य है और इसमें जानवर की तरह है। यह जानकारी प्रदान करने के लिए कि कुत्ते की माँ बदले में एक कुत्ता है, एक और घोषणा माँ: कुत्ता → कुत्ता जारी की जा सकती है; इसे फलन ओवर लोडिंग कहा जाता है, [[प्रोग्रामिंग भाषाओं में ओवरलोडिंग|प्रोग्रामिंग लैंग्वेज में ओवरलोडिंग]] के समान हो जाता है.
-[[क्रमबद्ध तर्क]] प्रत्येक पद के लिए एक सॉर्ट, या प्रकार निर्दिष्ट करने और एक सॉर्ट एस घोषित करने की अनुमति देता है<sub>1</sub> दूसरे प्रकार का एक उपवर्ग s<sub>2</sub>, सामान्यतः एस के रूप में लिखा जाता है<sub>1</sub> ⊆ एस<sub>2</sub>. उदाहरण के लिए, जैविक प्राणियों के बारे में तर्क करते समय, एक प्रकार के कुत्ते को एक प्रकार के जानवर का उपवर्ग घोषित करना उपयोगी होता है। जहां भी किसी प्रकार के शब्द की आवश्यकता होती है, उसके  समष्टि  पर किसी भी प्रकार के शब्द की आपूर्ति की जा सकती है।
-उदाहरण के लिए, एक फ़ंक्शन घोषणा मां: जानवर → जानवर, और एक निरंतर घोषणा लस्सी: कुत्ता मानते हुए, मां (लस्सी) शब्द पूरी प्रकार से मान्य है और इसमें जानवर की प्रकार है। यह जानकारी प्रदान करने के लिए कि कुत्ते की माँ बदले में एक कुत्ता है, एक और घोषणा माँ: कुत्ता → कुत्ता जारी की जा सकती है; इसे फ़ंक्शन ओवरलोडिंग कहा जाता है, [[प्रोग्रामिंग भाषाओं में ओवरलोडिंग]] के समान।
-[[क्रिस्टोफ़ वाल्थर]] ने क्रम-क्रमबद्ध तर्क में शब्दों के लिए एक एकीकरण एल्गोरिथ्म दिया, जिसके लिए किन्हीं दो घोषित प्रकारों की आवश्यकता होती है<sub>1</sub>, एस<sub>2</sub> उनका प्रतिच्छेदन एस<sub>1</sub> ∩ एस<sub>2</sub> घोषित किया जाना भी: यदि x<sub>1</sub> और एक्स<sub>2</sub> सॉर्ट का एक वेरिएबल है<sub>1</sub> और एस<sub>2</sub>, क्रमशः, समीकरण एक्स<sub>1</sub> ≐ एक्स<sub>2</sub> समाधान है {x<sub>1</sub> = एक्स, एक्स<sub>2</sub> = x }, जहां x: s<sub>1</sub> ∩ एस<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>
-उनके ढांचे में, उप-घोषणाएँ सम्मिश्र प्रकार की अभिव्यक्तियों के लिए प्रचारित की जाती हैं।
-एक प्रोग्रामिंग उदाहरण के रूप में, एक पैरामीट्रिक सॉर्ट सूची (X) घोषित की जा सकती है (टेम्प्लेट (C++)#Function templates|C++ टेम्प्लेट में X एक प्रकार का पैरामीटर है), और एक सबसॉर्ट घोषणा से int ⊆ संबंध सूची फ़्लोट करें (int ) ⊆ सूची (फ्लोट) का स्वचालित रूप से अनुमान लगाया जाता है, जिसका अर्थ है कि पूर्णांकों की प्रत्येक सूची भी फ्लोट्स की एक सूची है।
-श्मिट-शाउß ने शब्द घोषणाओं की अनुमति देने के लिए क्रम-क्रमबद्ध तर्क को सामान्यीकृत किया।
+[[पैरामीट्रिक बहुरूपता]] की अनुमति देने के लिए स्मोल्का ने क्रम-क्रमबद्ध लॉजिक को सामान्यीकृत किया जाता है।
+<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 ) ⊆ सूची (फ्लोट) का स्वचालित रूप से अनुमान लगाया जाता है, जिसका अर्थ है कि पूर्णांकों की प्रत्येक सूची भी फ्लोट्स की एक सूची है।
+श्मिट-शाउß ने शब्द घोषणाओं की अनुमति देने के लिए क्रम-क्रमबद्ध लॉजिक को सामान्यीकृत किया।
 <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 के लिए समीकरण हल करने वाले कलन विधि (उर्फ ''ई- एकीकरण एल्गोरिदम'') तैयार किए गए हैं;
+दूसरों के लिए यह सिद्ध हो चुका है कि ऐसा कोई कलन विधि उपलब्ध नहीं हो सकता है।
 उदाहरण के लिए, यदि {{mvar|a}} और {{mvar|b}} विशिष्ट स्थिरांक हैं,
-[[समीकरण]] {{tmath|x * a \doteq y * b}} का कोई समाधान नहीं है
-विशुद्ध [[वाक्यात्मक एकीकरण]] के संबंध में,
+[[समीकरण]] {{tmath|x * a \doteq y * b}} का कोई हल नहीं है.
+विशुद्ध वाक्यात्मकएकीकरण में संबंध हो जाता है
 जहां संचालक के बारे में कुछ भी पता नहीं चल पाया है {{tmath|*}}.
-चूंकि, यदि {{tmath|*}} क्रमविनिमेय माना जाता है,
+चूंकि यदि {{tmath|*}} क्रमविनिमेय माना जाता है,
 फिर प्रतिस्थापन {{math|{{mset|''x'' ↦ ''b'', ''y'' ↦ ''a''}}}} उपरोक्त समीकरण को हल करता है,
-तब से
+जब से,
 :{|
 |
@@ Line 336: / Line 368: @@
 | {{tmath|b * a}}
 |
-| by [[#Substitution|substitution application]]
+| प्रतिस्थापन अनुप्रयोग द्वारा
 |-
 | {{=}}
 | {{tmath|a * b}}
 |
-| by commutativity of {{tmath|*}}
+| की क्रमपरिवर्तनशीलता द्वारा {{tmath|*}}
 |-
 | {{=}}
 | {{tmath|y * b}}
 | {{math|{{mset|''x'' ↦ ''b'', ''y'' ↦ ''a''}}}}
-| by (converse) substitution application
+| (विपरीत) प्रतिस्थापन अनुप्रयोग द्वारा
 |}
-पृष्ठभूमि ज्ञान ई की क्रमपरिवर्तनशीलता बता सकता है {{tmath|*}} सार्वभौम समानता द्वारा{{tmath|1=u * v = v * u}} सभी के लिए {{math|''u'', ''v''}} .
+पृष्ठभूमि ज्ञान E की क्रम परिवर्तनशीलता बता सकता है {{tmath|*}} सार्वभौम समानता द्वारा{{tmath|1=u * v = v * u}} सभी के लिए {{math|''u'', ''v''}} .
-===विशेष पृष्ठभूमि ज्ञान सेट E===
+===विशेष पृष्ठभूमि ज्ञान समुच्चय E===
 {|
 |+ '''Used naming conventions'''
@@ Line 358: / Line 390: @@
 | {{tmath|(u*v)*w}}
 | align="center" | '''{{mvar|A}}'''
-| Associativity of {{tmath|*}}
+| की संबद्धता {{tmath|*}}
 |-
 | {{math|∀ ''u'',''v'':}}
@@ Line 365: / Line 397: @@
 | {{tmath|v*u}}
 | align="center" | '''{{mvar|C}}'''
-| Commutativity of {{tmath|*}}
+| की क्रमपरिवर्तनशीलता {{tmath|*}}
 |-
 | {{math|∀ ''u'',''v'',''w'':}}
@@ Line 372: / 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 379: / Line 416: @@
 | {{tmath|v*u+w*u}}
 | align="center" | '''{{mvar|D<sub>r</sub>}}'''
-| Right distributivity of {{tmath|*}} over {{tmath|+}}
+| का सही वितरण
+∗
+ऊपर
++
 |-
 | {{math|∀ ''u'':}}
@@ Line 386: / Line 428: @@
 | {{mvar|u}}
 | align="center" | '''{{mvar|I}}'''
-| Idempotence of {{tmath|*}}
+| नपुंसकताof {{tmath|*}}
 |-
 | {{math|∀ ''u'':}}
@@ Line 393: / 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 400: / 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 413: / Line 457: @@
 *{{mvar|C}}<ref>{{cite journal| author=F. Fages| title=साहचर्य-अनुकरणीय एकीकरण| journal=J. Symbolic Comput.| year=1987| volume=3| number=3| pages=257–275| doi=10.1016/s0747-7171(87)80004-4| url=https://hal.inria.fr/inria-00076271/file/RR-0287.pdf}}</ref>
 * [[बूलियन रिंग]]<ref>{{cite book| author=Martin, U., Nipkow, T.| chapter=Unification in Boolean Rings| title=Proc. 8th CADE| year=1986| volume=230| pages=506–513| publisher=Springer| editor=Jörg H. Siekmann| series=LNCS}}</ref><ref>{{cite journal|author1=A. Boudet |author2=J.P. Jouannaud |author3=M. Schmidt-Schauß | title=बूलियन रिंग्स और एबेलियन समूहों का एकीकरण| journal=Journal of Symbolic Computation| year=1989| volume=8|issue=5 | pages=449–477 | doi=10.1016/s0747-7171(89)80054-9| doi-access=free}}</ref>
-* एबेलियन समूह, यदि हस्ताक्षर को मनमाने ढंग से अतिरिक्त प्रतीकों द्वारा विस्तारित किया गया हो (लेकिन स्वयंसिद्ध नहीं)<ref name="Baader and Snyder 2001, p. 486">Baader and Snyder (2001), p. 486.</ref>
+* एबेलियन समूह, यदि हस्ताक्षर को यादृच्छिक ढंग से अतिरिक्त प्रतीकों द्वारा विस्तारित किया गया हो (लेकिन स्वयंसिद्ध नहीं)<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>
 निम्नलिखित सिद्धांतों के लिए एकीकरण अर्ध-निर्णायक है:
@@ Line 422: / Line 466: @@
 ===एकतरफा पैरामोड्यूलेशन===
-यदि ई के लिए एक [[अभिसरण शब्द पुनर्लेखन प्रणाली]] आर उपलब्ध है,
+यदि E के लिए एक [[अभिसरण शब्द पुनर्लेखन प्रणाली]] आर उपलब्ध है,
 'एकतरफा पैरामोड्यूलेशन' एल्गोरिदम<ref>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</ref>
-दिए गए समीकरणों के सभी समाधानों को गिनने के लिए उपयोग किया जा सकता है।
+दिए गए समीकरणों के सभी समाधानों के रूप में गिनने के लिए उपयोग किया जा सकता है।
 {| style="border: 1px solid darkgray;"
-|+ One-sided paramodulation rules
+|+ एकतरफ़ा पैरामॉड्यूलेशन नियम
 |- border="0"
 | align="right" | ''G'' ∪ { ''f''(''s''<sub>1</sub>,...,''s''<sub>''n''</sub>) ≐ ''f''(''t''<sub>1</sub>,...,''t''<sub>''n''</sub>) }
-| ; ''S''
+|  ; ''S''
 | ⇒
 | align="right" | ''G'' ∪ { ''s''<sub>1</sub> ≐ ''t''<sub>1</sub>, ..., ''s''<sub>''n''</sub> ≐ ''t''<sub>''n''</sub> }
-| ''; ''S''
+| ''; ''S
 |
 | &nbsp; &nbsp; '''decompose'''
 |-
 | align="right" | ''G'' ∪ { ''x'' ≐ ''t'' }
-| ; ''S''
+|  ; ''S''
 | ⇒
 | align="right" | ''G'' { ''x'' ↦ ''t'' }
@@ Line 446: / Line 492: @@
 |-
 | align="right" | ''G'' ∪ { ''f''(''s''<sub>1</sub>,...,''s''<sub>''n''</sub>) ≐ ''t'' }
-| ; ''S''
+|  ; ''S''
 | ⇒
 | align="right" | ''G'' ∪ { ''s''<sub>1</sub> ≐ u<sub>1</sub>, ..., ''s''<sub>''n''</sub> ≐ u<sub>''n''</sub>, ''r'' ≐ ''t'' }
-| ; ''S''
+|  ; ''S''
 | align="right" | &nbsp; &nbsp; if ''f''(''u''<sub>1</sub>,...,''u''<sub>''n''</sub>) → ''r'' is a rule from ''R''
 | &nbsp; &nbsp; '''mutate'''
 |-
 | align="right" | ''G'' ∪ { ''f''(''s''<sub>1</sub>,...,''s''<sub>''n''</sub>) ≐ ''y'' }
-| ; ''S''
+|  ; ''S''
 |⇒
 | align="right" | ''G'' ∪ { ''s''<sub>1</sub> ≐ ''y''<sub>1</sub>, ..., ''s''<sub>''n''</sub> ≐ ''y''<sub>''n''</sub>, ''y'' ≐ ''f''(''y''<sub>1</sub>,...,''y''<sub>''n''</sub>) }
-| ; ''S''
+|  ; ''S''
 | align="right" | if ''y''<sub>1</sub>,...,''y''<sub>''n''</sub> are new variables
 | &nbsp; &nbsp; '''imitate'''
 |}
-जी से प्रारंभ करके हल की जाने वाली एकीकरण समस्या और एस पहचान प्रतिस्थापन है, नियमों को गैर-नियतात्मक रूप से लागू किया जाता है जब तक कि खाली सेट वास्तविक जी के रूप में प्रकट नहीं होता है, इस स्थिति में वास्तविक एस एक एकीकृत प्रतिस्थापन है। आदेश के आधार पर पैरामॉड्यूलेशन नियम लागू होते हैं, जी से वास्तविक समीकरण की पसंद पर, और आर की पसंद पर{{'}}के नियमों में परिवर्तन, विभिन्न संगणना पथ संभव हैं। मात्र कुछ ही समाधान की ओर ले जाते हैं, जबकि अन्य G ≠ {} पर समाप्त होते हैं जहां कोई और नियम लागू नहीं होता है (जैसे G = { f(...) ≐ g(...) })।
+''G'' से प्रारंभ करके हल की जाने वाली एकीकरण समस्या और S पहचान प्रतिस्थापन है, नियमों को गैर-नियतात्मक रूप से प्रयुक्त किया जाता है, जब तक कि खाली समुच्चय वास्तविक ''G'' के रूप में प्रकट नहीं होता है, इस स्थिति में वास्तविक S एक एकीकृत प्रतिस्थापन है। आदेश के आधार पर पैरामॉड्यूलेशन नियम प्रयुक्त होते हैं, ''G'' से वास्तविक समीकरण की पसंद पर और ''R'' की पसंद पर{{'}}के नियमों में परिवर्तन, विभिन्न संगणना पथ संभव हैं। मात्र कुछ ही हल की ओर ले जाते हैं, जबकि अन्य G ≠ {} पर समाप्त होते हैं, जहां कोई और नियम प्रयुक्त नहीं होता है. (जैसे G = { f(...) ≐ g(...) })।
 {| style="border: 1px solid darkgray;"
@@ Line 474: / Line 520: @@
 | → ''x''.''app''(''y'',''z'')
 |}
-उदाहरण के लिए, एक शब्द रीराइट सिस्टम आर का उपयोग विपक्ष और शून्य से निर्मित सूचियों के परिशिष्ट ऑपरेटर को परिभाषित करने के लिए किया जाता है; जहां संक्षिप्तता के लिए 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)। पैरामोड्यूलेशन एल्गोरिदम उदाहरण आर के साथ दिए जाने पर उस ई के संबंध में समीकरणों के समाधान की गणना करता है।
+उदाहरण के लिए, ऐप(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 } प्राप्त किया जा सकता है। वास्तव में,
+ऐप(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 दी गई समस्या का हल करता है।
-एकीकरण समस्या {app(x,app(y,x)) ≐ a.a.nil } के लिए एक सफल उदाहरण गणना पथ नीचे दिखाया गया है। परिवर्तनीय नाम टकराव से बचने के लिए, नियम परिवर्तन द्वारा उनके उपयोग से पहले हर बार पुनर्लेखन नियमों का लगातार नाम बदला जाता है; वी<sub>2</sub>, में<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 दी गई समस्या का समाधान करता है।
 दूसरा सफल संगणना पथ, जिसे 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 490: / 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> }
+| { ''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> }
+| { ''x'' ↦ ''a''.''v''<sub>3</sub> }
 |-
 | mutate(1) || ⇒
 | { ''y'' ≐ ''nil'', ''a''.''v''<sub>3</sub> ≐ ''v''<sub>5</sub>, {{color|red|''v''<sub>5</sub> ≐ ''v''<sub>4</sub>}}, ''app''(''v''<sub>3</sub>,''v''<sub>4</sub>) ≐ ''a''.''nil'' }
-| { ''x'' ↦  ''a''.''v''<sub>3</sub> }
+| { ''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> }
+| { ''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> }
+| { ''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> }
+| { ''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> }
+| { ''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'' }
+| { ''y'' ↦ ''nil'', ''x'' ↦ ''a''.''nil'' }
 |-
-| eliminate || ⇒
+| एलिमिनेट || ⇒
 | { {{color|red|''a''.''nil'' ≐ ''a''.''nil''}} }
-| { ''y'' ↦ ''nil'', ''x'' ↦  ''a''.''nil'' }
+| { ''y'' ↦ ''nil'', ''x'' ↦ ''a''.''nil'' }
 |-
-| decompose || ⇒
+| डीकोम्पोस || ⇒
 | { {{color|red|''a'' ≐ ''a''}}, ''nil'' ≐ ''nil'' }
-| { ''y'' ↦ ''nil'', ''x'' ↦  ''a''.''nil'' }
+| { ''y'' ↦ ''nil'', ''x'' ↦ ''a''.''nil'' }
 |-
-| decompose || ⇒
+| डीकोम्पोस || ⇒
 | { {{color|red|''nil'' ≐ ''nil''}} }
-| { ''y'' ↦ ''nil'', ''x'' ↦  ''a''.''nil'' }
+| { ''y'' ↦ ''nil'', ''x'' ↦ ''a''.''nil'' }
 |-
-| decompose &nbsp; &nbsp; || ⇒ &nbsp; &nbsp;
+| डीकोम्पोस || ⇒ &nbsp; &nbsp;
 | {}
-| { ''y'' ↦ ''nil'', ''x'' ↦  ''a''.''nil'' }
+| { ''y'' ↦ ''nil'', ''x'' ↦ ''a''.''nil'' }
 |}
@@ Line 551: / Line 600: @@
 [[File:Triangle diagram of narrowing step svg.svg|thumb|पुनर्लेखन नियम का उपयोग करते हुए एकीकृत प्रतिस्थापन σ (निचली पंक्ति) के साथ, पद s में स्थिति p पर चरण s ↝ t को संकीर्ण करने का त्रिभुज आरेख {{math|1=''l'' → ''r''}} (सबसे ऊपर की कतार)]]यदि R, E के लिए एक अभिसारी पद पुनर्लेखन प्रणाली है,
 पिछले अनुभाग के लिए एक दृष्टिकोण विकल्प में 'संकीर्ण चरणों' का क्रमिक अनुप्रयोग सम्मिलित है;
 यह अंततः किसी दिए गए समीकरण के सभी समाधानों की गणना करेगा।
-एक संकीर्ण चरण (cf. चित्र) में सम्मिलित है
-* वर्तमान पद का एक गैर-परिवर्तनीय उपपद चुनना,
+एक संकीर्ण चरण (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 के रूप में निरूपित की जाती है।
+* तात्कालिक नियम के दाहिने हाथ को तात्कालिक शब्द में बदलना होता है।
-सहज रूप से, संकीर्ण चरणों का एक क्रम टी<sub>1</sub> ↝ टी<sub>2</sub> ↝ ... ↝ टी<sub>''n''</sub> इसे पुनः लिखने के चरणों के अनुक्रम के रूप में सोचा जा सकता है<sub>1</sub> → टी<sub>2</sub> → ... → टी<sub>''n''</sub>, लेकिन प्रारंभिक पद t के साथ<sub>1</sub> प्रत्येक प्रयुक्त नियम को लागू करने के लिए आवश्यकतानुसार इसे और अधिक त्वरित किया जा रहा है।
+फॉर्मल रूप से, यदि {{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> प्रत्येक प्रयुक्त नियम को प्रयुक्त करने के लिए आवश्यकतानुसार इसे और अधिक त्वरित किया जा रहा है।
 #एकतरफा पैरामॉड्यूलेशन उदाहरण पैरामॉड्यूलेशन गणना निम्नलिखित संकीर्ण अनुक्रम से मेल खाती है (↓ यहां तात्कालिकता का संकेत है):
@@ Line 577: / 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}}''}}.
-औपचारिक रूप से: जब भी {{math|1=''sσ'' {{underset|&lowast;|→}} ''t''}} कुछ प्रतिस्थापन के लिए σ रखता है, तो वहां शर्तें उपलब्ध हैं {{math|''s{{prime}}'', ''t{{prime}}''}} ऐसा है कि {{math|''s'' {{underset|&lowast;|↝}} ''s{{prime}}''}} और {{math|''t'' {{underset|&lowast;|→}} ''t{{prime}}''}} और {{math|1=''s{{prime}}'' ''τ'' = ''t{{prime}}''}} कुछ प्रतिस्थापन के लिए τ.
+फॉर्मल रूप से: जब भी {{math|1=''sσ'' {{underset|&lowast;|→}} ''t''}} कुछ प्रतिस्थापन के लिए σ रखता है, तो वहां शर्तें उपलब्ध हैं {{math|''s{{prime}}'', ''t{{prime}}''}} ऐसा है कि {{math|''s'' {{underset|&lowast;|↝}} ''s{{prime}}''}} और {{math|''t'' {{underset|&lowast;|→}} ''t{{prime}}''}} और {{math|1=''s{{prime}}'' ''τ'' = ''t{{prime}}''}} कुछ प्रतिस्थापन के लिए τ.
 ==उच्च-क्रम एकीकरण==
-[[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. डी(बी,एक्स,सी) },
+{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>
+अभिकलनात्मक लैंग्वेज विज्ञान में [[अण्डाकार निर्माण]] के सबसे प्रभावशाली सिद्धांतों में से एक यह है कि दीर्घवृत्त को मुक्त चर द्वारा दर्शाया जाता है, जिनके मान तब उच्च-क्रम एकीकरण का उपयोग करके निर्धारित किए जाते हैं। उदाहरण के लिए जॉन का अर्थपूर्ण प्रतिनिधित्व मैरी को पसंद है और पीटर को भी पसंद है {{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 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>
-[[वेन स्नाइडर]] ने उच्च-क्रम एकीकरण और ई-एकीकरण दोनों का सामान्यीकरण दिया, अर्थात लैम्ब्डा-शब्द मॉड्यूलो को एक समीकरण सिद्धांत को एकीकृत करने के लिए एक एल्गोरिदम।<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 599: / Line 655: @@
 *[[लैम्ब्डा कैलकुलस]] में [[स्पष्ट प्रतिस्थापन]]
 *गणितीय [[समीकरण हल करना]]
-*डिस-यूनिफिकेशन (कंप्यूटर विज्ञान)|डिस-यूनिफिकेशन: प्रतीकात्मक अभिव्यक्ति के बीच असमानताओं को हल करना
+*डिस- एकीकरण (कंप्यूटर विज्ञान)|डिस-यूनिफिकेशन: सिंबॉलिक अभिव्यक्तियों के बीच असमानताओं को हल करना
-*एंटी-यूनिफिकेशन (कंप्यूटर साइंस)|एंटी-यूनिफिकेशन: दो शब्दों के कम से कम सामान्य सामान्यीकरण (एलजीजी) की गणना करना, सबसे सामान्य उदाहरण (एमजीयू) की गणना करना
+*एंटी- एकीकरण (कंप्यूटर साइंस)|एंटी-यूनिफिकेशन: दो शब्दों के कम से कम सामान्य सामान्यीकरण (एलजीजी) की गणना करना, सबसे सामान्य उदाहरण (एमजीयू) की गणना करना
 *सब्समिशन जाली, एक जाली जिसमें मिलन के रूप में एकीकरण और जुड़ने के रूप में विरोधी एकीकरण होता है
 *ओन्टोलॉजी संरेखण ([[शब्दार्थ तुल्यता]] के साथ एकीकरण का उपयोग करें)
@@ Line 624: / 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