प्रोग्राम सिंथेसिस: Difference between revisions

Latest revision as of 16:08, 11 April 2023

कंप्यूटर विज्ञान में, प्रोग्राम सिंथेसिस एक ऐसा कार्यक्रम बनाने का कार्य है किसी दिए गए उच्च-स्तरीय औपचारिक विनिर्देश को प्रमाणित करता है। कार्यक्रम सत्यापन के विपरीत, कार्यक्रम दिए जाने के बजाय निर्मित किया जाना है; तथापि, दोनों क्षेत्र औपचारिक प्रमाण तकनीकों का उपयोग करते हैं, और दोनों में स्वचालितकरण की विभिन्न डिग्री के दृष्टिकोण सम्मिलित हैं। स्वचालित प्रोग्रामिंग तकनीकों के विपरीत, प्रोग्राम सिंथेसिस में विनिर्देश सामान्यतः एक उपयुक्त तार्किक कलन में गैर-एल्गोरिदमिक कथन होते हैं।^[1]

उत्पत्ति

1957 में कॉर्नेल विश्वविद्यालय में समर इंस्टीट्यूट ऑफ सिंबॉलिक लॉजिक के दौरान, अलोंजो चर्च ने गणितीय आवश्यकताओं से एक सर्किट को संश्लेषित करने की समस्या को परिभाषित किया।^[2] भले ही काम केवल सर्किट को संदर्भित करता है और कार्यक्रम को नहीं, काम को प्रोग्राम सिंथेसिस के प्रारंभिक विवरणों में से एक माना जाता है और कुछ शोधकर्ता प्रोग्राम सिंथेसिस को "चर्च की समस्या" के रूप में संदर्भित करते हैं। 1960 के दशक में, आर्टिफिशियल इंटेलिजेंस में शोधकर्ताओं द्वारा "स्वचालित प्रोग्रामर" के लिए एक समान विचार की खोज की गई थी।^{[citation needed]}

तब से, विभिन्न अनुसंधान समुदायों ने प्रोग्राम सिंथेसिस की समस्या पर विचार किया। उल्लेखनीय कार्यों में बुच्ची और लैंडवेबर द्वारा 1969 ऑटोमेटा-सैद्धांतिक दृष्टिकोण,^[3] और मन्ना और वाल्डिंगर (सी। 1980) द्वारा कार्य सम्मिलित हैं। आधुनिक उच्च-स्तरीय प्रोग्रामिंग भाषाओं के विकास को प्रोग्राम सिंथेसिस के एक रूप के रूप में भी समझा जा सकता है।

21वीं सदी के घटनाक्रम

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

मन्ना और वाल्डिंगर की रूपरेखा

गैर-क्लॉज़ल रिज़ॉल्यूशन नियम (एकीकृत प्रतिस्थापन नहीं दिखाए गए)
एनआर	अभिकथन	लक्ष्य	कार्यक्रम	मूल
51	$E[p]$
52	$F[p]$
53		$G[p]$	s
54		$H[p]$	t
55	$E[{\text{true}}]\lor F[{\text{false}}]$			संकल्प(51,52)
56		$\lnot F[{\text{true}}]\land G[{\text{false}}]$	s	संकल्प(52,53)
57		$\lnot F[{\text{false}}]\land G[{\text{true}}]$	s	संकल्प(53,52)
58		$G[{\text{true}}]\land H[{\text{false}}]$	p ? s : t	संकल्प(53,54)

1980 में प्रकाशित मन्ना और वाल्डिंगर का ढांचा,^[7]^[8] उपयोगकर्ता द्वारा दिए गए पहले-क्रम विनिर्देश सूत्र से प्रारंभ होता है। उस सूत्र के लिए, एक प्रमाण का निर्माण किया जाता है, जिससे एक कार्यात्मक कार्यक्रम को एकीकृत प्रतिस्थापन से भी संश्लेषित किया जाता है।

ढांचे को तालिका लेआउट में प्रस्तुत किया गया है, जिसमें कॉलम सम्मिलित हैं:

संदर्भ उद्देश्यों के लिए एक पंक्ति संख्या ("एनआर")।
सूत्र जो पहले से ही स्थापित किए जा चुके हैं, जिनमें स्वयंसिद्ध और पूर्व शर्त सम्मिलित हैं, ("अभिकथन")
फॉर्मूले अभी भी सिद्ध होने बाकी हैं, पोस्टकंडिशन (लक्ष्य),^{[note 1]} सम्मिलित हैं
वैध आउटपुट वैल्यू ("प्रोग्राम") को दर्शाने वाली शर्तें^{[note 2]}
वर्तमान पंक्ति के लिए एक औचित्य ("उत्पत्ति")

प्रारंभ में, पृष्ठभूमि ज्ञान, पूर्व-शर्तें और पश्च-शर्तें तालिका में दर्ज की जाती हैं। उसके बाद, उपयुक्त प्रमाण नियम मैन्युअल रूप से लागू किए जाते हैं। ढांचे को मध्यवर्ती सूत्रों की मानव पठनीयता को बढ़ाने के लिए डिज़ाइन किया गया है: शास्त्रीयसंकल्प के विपरीत, इसे क्लॉसल सामान्य रूप की आवश्यकता नहीं होती है, लेकिन मनमाना संरचना के सूत्रों के साथ तर्क करने की अनुमति देता है और किसी भी जंक्शनर्स ("गैर-खंड संकल्प") को सम्मिलित करता है। प्रमाण कब पूरा होता है ${\it {true}}$ लक्ष्य स्तंभ में व्युत्पन्न किया गया है, या, समकक्ष रूप से, ${\it {false}}$ अभिकथन कॉलम में। इस दृष्टिकोण से प्राप्त कार्यक्रम से प्रारंभ होने वाले विनिर्देश सूत्र को पूरा करने की गारंटी है; इस अर्थ में वे निर्माण द्वारा सही हैं।^[9] केवल एक न्यूनतावादी, अभी तक ट्यूरिंग-पूर्ण,^[10] विशुद्ध रूप से कार्यात्मक प्रोग्रामिंग भाषा, जिसमें सशर्त, पुनरावर्तन और अंकगणित और अन्य ऑपरेटर सम्मिलित हैं^{[note 3]} समर्थित है। इस ढांचे के भीतर किए गए मामले के अध्ययन ने गणना करने के लिए एल्गोरिदम को संश्लेषित किया उदाहरण के लिए विभाजन, शेष,^[11] वर्गमूल,^[12] एकीकरण,^[13] संबंधपरक डेटाबेस प्रश्नों के उत्तर^[14] और कई छँटाई एल्गोरिदम।^[15]^[16]

प्रमाण नियम

प्रमाण नियमों में सम्मिलित हैं:

नॉन-क्लॉज़ल रेज़ोल्यूशन (तालिका देखें)।

उदाहरण के लिए, अभिकथन सूत्रों को हल करके पंक्ति 55 प्राप्त की जाती है

E

51 से और

F

52 से जो दोनों कुछ सामान्य उपसूत्र साझा करते हैं

p

. विलायक के विघटन के रूप में बनता है

E

, साथ

p

द्वारा प्रतिस्थापित किया गया

{\it {true}}

, और

F

, साथ

p

द्वारा प्रतिस्थापित किया गया

{\it {false}}

। यह विलायक तार्किक रूप से के संयोजन से अनुसरण करता है

E

और

F

। अधिक सामान्यतः,

E

और

F

को केवल दो अविवेकी उपसूत्रों की आवश्यकता है

p_{1}

और

p_{2}

, क्रमश; उनके विलायक तब से बनते हैं

E\theta

और

F\theta

पहले की तरह, जहाँ

\theta

का सबसे सामान्य एकीकृतकर्ता है

p_{1}

और

p_{2}

। यह नियम खंडों के समाधान का सामान्यीकरण करता है। ^[17]

रिज़ॉल्वेंट के आउटपुट को बनाने के लिए पैरेंट फ़ार्मुलों के प्रोग्राम टर्म्स को लाइन 58 में दिखाए अनुसार संयोजित किया जाता है। सामान्य मामले में,

\theta

बाद वाले पर भी लागू होता है। सबफॉर्मूला के बाद से

p

आउटपुट में दिखाई देता है, गणना योग्य गुणों के अनुरूप केवल उप सूत्रों पर हल करने के लिए देखभाल की जानी चाहिए।

तार्किक परिवर्तन।

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

E\land (F\lor G)

को रूपांतरित किया जा सकता है

(E\land F)\lor (E\land G)

) अभिकथन और साथ ही लक्ष्यों में, क्योंकि दोनों समान हैं।

संयोजक अभिकथनों और वियोजनात्मक लक्ष्यों का विभाजन।

एक उदाहरण नीचे दिए गए खिलौने के उदाहरण की 11 से 13 पंक्तियों में दिखाया गया है।

संरचनात्मक प्रेरण।

यह नियम पुनरावर्ती कार्यों के संश्लेषण की अनुमति देता है। किसी दिए गए पूर्व और बाद की स्थिति के लिए "दिया गया

x

ऐसा है कि

{\textit {pre}}(x)

, ढूंढें

f(x)=y

ऐसा है कि

{\textit {post}}(x,y)

", और एक उपयुक्त उपयोगकर्ता द्वारा दिया गया सुव्यवस्थित आदेश

\prec

के डोमेन

x

, एक अभिकथन जोड़ना हमेशा अच्छा होता है

x'\prec x\land {\textit {pre}}(x')\implies {\textit {post}}(x',f(x'))

.^[18] इस अभिकथन के साथ समाधान करने के लिए एक पुनरावर्ती कॉल प्रस्तुत कर सकता है

f

कार्यक्रम अवधि में।

मन्ना, वाल्डिंगर (1980), पृष्ठ 108-111 में एक उदाहरण दिया गया है, जहां दो दिए गए पूर्णांकों के भागफल और शेष की गणना करने के लिए एक एल्गोरिथ्म को अच्छी तरह से क्रम का उपयोग करके संश्लेषित किया जाता है।

(n',d')\prec (n,d)

द्वारा परिभाषित

0\leq n'<n

(पृष्ठ 110)।

मुर्रे ने इन नियमों को प्रथम-क्रम तर्क के लिए पूर्ण दिखाया है।^[19] 1986 में, मन्ना और वाल्डिंगर ने समानता को संभालने के लिए सामान्यीकृत ई-रिज़ॉल्यूशन और पैरामॉड्यूलेशन नियम जोड़े;^[20] बाद में, ये नियम अधूरे निकले (लेकिन फिर भी सही थे)।^[21]

उदाहरण

अधिकतम कार्य का उदाहरण संश्लेषण
एनआर	अभिकथन	लक्ष्य	कार्यक्रम	मूल
1	$A=A$			सिद्ध प्रमाण
2	$A\leq A$			सिद्ध प्रमाण
3	$A\leq B\lor B\leq A$			सिद्ध प्रमाण
10		$x\leq M\land y\leq M\land (x=M\lor y=M)$	M	विशेष विवरण
11		$(x\leq M\land y\leq M\land x=M)\lor (x\leq M\land y\leq M\land y=M)$	M	डीआईएसटीआर(10)
12		$x\leq M\land y\leq M\land x=M$	M	विभाजित करना(11)
13		$x\leq M\land y\leq M\land y=M$	M	विभाजित करना(11)
14		$x\leq x\land y\leq x$	x	संकल्प(12,1)
15		$y\leq x$	x	संकल्प(14,2)
16		$\lnot (x\leq y)$	x	संकल्प(15,3)
17		$x\leq y\land y\leq y$	y	संकल्प(13,1)
18		$x\leq y$	y	संकल्प(17,2)
19		${\textit {true}}$	x<y ? y : x	संकल्प(18,16)

एक खिलौना उदाहरण के रूप में, अधिकतम गणना करने के लिए एक कार्यात्मक प्रोग्राम दो नंबर का $M$ $x$ और $y$ को निम्नानुसार प्राप्त किया जा सकता है।^{[citation needed]}

आवश्यकता विवरण से प्रारंभ करते हुए "अधिकतम किसी भी संख्या से बड़ा या उसके बराबर है, और दी गई संख्याओं में से एक है", प्रथम-क्रम सूत्र $\forall X\forall Y\exists M:X\leq M\land Y\leq M\land (X=M\lor Y=M)$ इसके औपचारिक अनुवाद के रूप में प्राप्त किया जाता है। इस सूत्र को सिद्ध करना है। रिवर्स विद्वता द्वारा,^{[note 4]} पंक्ति 10 में विशेष विवरण प्राप्त किया गया है, क्रमशः एक चर और एक स्कोलेम स्थिरांक को दर्शाते हुए एक बड़े और छोटे अक्षर।

पंक्ति 11 में वितरण नियम के लिए रूपांतरण नियम लागू करने के बाद, प्रमाण लक्ष्य एक संयोजन है, और इसलिए इसे दो मामलों में विभाजित किया जा सकता है, अर्थात। लाइन 12 और 13।

पहले मामले की ओर मुड़ते हुए, पंक्ति 12 को पंक्ति 1 में सिद्ध प्रमाण के साथ हल करने से कार्यक्रम चर की तात्कालिकता होती है $M$ पंक्ति 14 में। सहज रूप से, पंक्ति 12 का अंतिम संयोजन मूल्य निर्धारित करता है $M$ इस मामले में लेना चाहिए। औपचारिक रूप से, उपरोक्त पंक्ति 57 में दिखाया गया गैर-खंड संकल्प नियम 12 और 1 पंक्तियों पर लागू होता है

$p$ का $A=A$ और $x=M$ का सामान्य उदाहरण $x=x$ है, जो बाद के सूत्रों को वाक्यगत रूप से एकीकृत करके प्राप्त किया गया है,
$F[$ $p$ $]$ $true \land$ $x=x$ , तात्कालिक पंक्ति 1 से प्राप्त किया गया है (उचित रूप से पैड किया गया है ताकि संदर्भ $F[\cdot]$ को $p$ के आसपास दिखाई दे), और
$G[$ $p$ $]$ $x \leq x \land y \leq x \land$ $x = x$ , होने के नाते, तत्काल रेखा 12 से प्राप्त किया गया है,

उपज $\lnot ($ $true \land$ $false$ $) \land ($ $x \leq x \land y \leq x \land$ $true$ $)$ , जो करने के लिए सरल करता है $x\leq x\land y\leq x$ .

इसी तरह, लाइन 14 से लाइन 15 और फिर लाइन 16 रेजोल्यूशन से मिलती है। साथ ही, दूसरा मामला, $x\leq M\land y\leq M\land y=M$ लाइन 13 में, इसी तरह से संभाला जाता है, अंत में लाइन 18 देता है।

अंतिम चरण में, दोनों स्थितियाँ (यानी पंक्तियाँ 16 और 18) जुड़ जाती हैं, पंक्ति 58 से संकल्प नियम का उपयोग करते हुए; उस नियम को लागू करने के लिए प्रारंभिक चरण 15→16 की आवश्यकता थी। सहज रूप से, पंक्ति 18 को "मामले में" के रूप में पढ़ा जा सकता है $x\leq y$ , उत्पादन $y$ मान्य है; चरण 15→16 ने स्थापित किया कि दोनों मामले 16 और 18 पूरक हैं।^{[note 5]} चूँकि दोनों पंक्तियाँ 16 और 18 एक कार्यक्रम शब्द के साथ आती हैं, एक सशर्त अभिव्यक्ति का परिणाम प्रोग्राम कॉलम में होता है। लक्ष्य सूत्र के बाद से ${\textit {true}}$ व्युत्पन्न किया गया है, प्रमाण दिया गया है, और का कार्यक्रम स्तंभ ${\textit {true}}$ पंक्ति में कार्यक्रम है।

यह भी देखें

↑ The distinction "Assertions" / "Goals" is for convenience only; following the paradigm of proof by contradiction, a Goal $F$ is equivalent to an assertion $\lnot F$ .
↑ When $F$ and $s$ is the Goal formula and the Program term in a line, respectively, then in all cases where $F$ holds, $s$ is a valid output of the program to be synthesized. This invariant is maintained by all proof rules. An Assertion formula usually is not associated with a Program term.
↑ Only the conditional operator (?:) is supported from the beginning. However, arbitrary new operators and relations can be added by providing their properties as axioms. In the toy example below, only the properties of $=$ and $\leq$ that are actually needed in the proof have been axiomatized, in line 1 to 3.
↑ While ordinary Skolemization preserves satisfiability, reverse Skolemization, i.e. replacing universally quantified variables by functions, preserves validity.
↑ Axiom 3 was needed for that; in fact, if $\leq$ wasn't a total order, no maximum could be computed for uncomparable inputs $x,y$ .

संदर्भ

↑ Basin, D.; Deville, Y.; Flener, P.; Hamfelt, A.; Fischer Nilsson, J. (2004). "Synthesis of programs in computational logic". In M. Bruynooghe and K.-K. Lau (ed.). कम्प्यूटेशनल लॉजिक में प्रोग्राम डेवलपमेंट. LNCS. Vol. 3049. Springer. pp. 30–65. CiteSeerX 10.1.1.62.4976.
↑ Alonzo Church (1957). "परिपथ संश्लेषण की समस्या के लिए पुनरावर्ती अंकगणित के अनुप्रयोग". Summaries of the Summer Institute of Symbolic Logic. 1: 3–50.
↑ Richard Büchi, Lawrence Landweber (Apr 1969). "परिमित-राज्य रणनीतियों द्वारा अनुक्रमिक स्थितियों को हल करना". Transactions of the American Mathematical Society. 138: 295–311. doi:10.2307/1994916. JSTOR 1994916.
↑ Solar-Lezama, Armando (2008). स्केचिंग द्वारा प्रोग्राम संश्लेषण (PDF) (Ph.D.). University of California, Berkeley.
↑ Alur, Rajeev; al., et (2013). "सिंटेक्स-निर्देशित संश्लेषण". Proceedings of Formal Methods in Computer-Aided Design. IEEE. p. 8.
↑ SyGuS-Comp (Syntax-Guided Synthesis Competition)
↑ Zohar Manna, Richard Waldinger (Jan 1980). "कार्यक्रम संश्लेषण के लिए एक निगमनात्मक दृष्टिकोण". ACM Transactions on Programming Languages and Systems. 2: 90–121. doi:10.1145/357084.357090. S2CID 14770735.
↑ Zohar Manna and Richard Waldinger (Dec 1978). कार्यक्रम संश्लेषण के लिए एक निगमनात्मक दृष्टिकोण (PDF) (Technical Note). SRI International. Archived (PDF) from the original on January 27, 2021.
↑ See Manna, Waldinger (1980), p.100 for correctness of the resolution rules.
↑ Boyer, Robert S.; Moore, J. Strother (May 1983). शुद्ध लिस्प की ट्यूरिंग पूर्णता का एक यांत्रिक प्रमाण (PDF) (Technical report). Institute for Computing Science, University of Texas at Austin. 37. Archived (PDF) from the original on 22 September 2017.
↑ Manna, Waldinger (1980), p.108-111
↑ Zohar Manna and Richard Waldinger (Aug 1987). "एक द्विआधारी-खोज प्रतिमान की उत्पत्ति". Science of Computer Programming. 9 (1): 37–83. doi:10.1016/0167-6423(87)90025-6.
↑ Daniele Nardi (1989). "निगमनात्मक-झांकी विधि द्वारा एक एकीकरण एल्गोरिथम का औपचारिक संश्लेषण". Journal of Logic Programming. 7: 1–43. doi:10.1016/0743-1066(89)90008-3.
↑ Daniele Nardi and Riccardo Rosati (1992). "Deductive Synthesis of Programs for Query Answering". In Kung-Kiu Lau and Tim Clement (ed.). तर्क कार्यक्रम संश्लेषण और परिवर्तन पर अंतर्राष्ट्रीय कार्यशाला (LOPSTR). Workshops in Computing. Springer. pp. 15–29. doi:10.1007/978-1-4471-3560-9_2.
↑ Jonathan Traugott (1986). "Deductive Synthesis of Sorting Programs". स्वचालित कटौती पर अंतर्राष्ट्रीय सम्मेलन की कार्यवाही. LNCS. Vol. 230. Springer. pp. 641–660.
↑ Jonathan Traugott (Jun 1989). "छँटाई कार्यक्रमों का निगमनात्मक संश्लेषण". Journal of Symbolic Computation. 7 (6): 533–572. doi:10.1016/S0747-7171(89)80040-9.
↑ Manna, Waldinger (1980), p.99
↑ Manna, Waldinger (1980), p.104
↑ Manna, Waldinger (1980), p.103, referring to: Neil V. Murray (Feb 1979). A Proof Procedure for Quantifier-Free Non-Clausal First Order Logic (Technical report). Syracuse Univ. 2-79.
↑ Zohar Manna, Richard Waldinger (Jan 1986). "स्वचालित कटौती में विशेष संबंध". Journal of the ACM. 33: 1–59. doi:10.1145/4904.4905. S2CID 15140138.
↑ Zohar Manna, Richard Waldinger (1992). "The Special-Relations Rules are Incomplete". प्रक्रिया। सीएडीई 11. LNCS. Vol. 607. Springer. pp. 492–506.

Zohar Manna, Richard Waldinger (1975). "Knowledge and Reasoning in Program Synthesis". Artificial Intelligence. 6 (2): 175–208. doi:10.1016/0004-3702(75)90008-9.

[9] The distinction "Assertions" / "Goals" is for convenience only; following the paradigm of proof by contradiction, a Goal $F$ is equivalent to an assertion $\lnot F$ .

[10] When $F$ and $s$ is the Goal formula and the Program term in a line, respectively, then in all cases where $F$ holds, $s$ is a valid output of the program to be synthesized. This invariant is maintained by all proof rules. An Assertion formula usually is not associated with a Program term.

[13] Only the conditional operator (?:) is supported from the beginning. However, arbitrary new operators and relations can be added by providing their properties as axioms. In the toy example below, only the properties of $=$ and $\leq$ that are actually needed in the proof have been axiomatized, in line 1 to 3.

[25] While ordinary Skolemization preserves satisfiability, reverse Skolemization, i.e. replacing universally quantified variables by functions, preserves validity.

[26] Axiom 3 was needed for that; in fact, if $\leq$ wasn't a total order, no maximum could be computed for uncomparable inputs $x,y$ .

[1] Basin, D.; Deville, Y.; Flener, P.; Hamfelt, A.; Fischer Nilsson, J. (2004). "Synthesis of programs in computational logic". In M. Bruynooghe and K.-K. Lau (ed.). कम्प्यूटेशनल लॉजिक में प्रोग्राम डेवलपमेंट. LNCS. Vol. 3049. Springer. pp. 30–65. CiteSeerX 10.1.1.62.4976.

[2] Alonzo Church (1957). "परिपथ संश्लेषण की समस्या के लिए पुनरावर्ती अंकगणित के अनुप्रयोग". Summaries of the Summer Institute of Symbolic Logic. 1: 3–50.

[3] Richard Büchi, Lawrence Landweber (Apr 1969). "परिमित-राज्य रणनीतियों द्वारा अनुक्रमिक स्थितियों को हल करना". Transactions of the American Mathematical Society. 138: 295–311. doi:10.2307/1994916. JSTOR 1994916.

[4] Solar-Lezama, Armando (2008). स्केचिंग द्वारा प्रोग्राम संश्लेषण (PDF) (Ph.D.). University of California, Berkeley.

[5] Alur, Rajeev; al., et (2013). "सिंटेक्स-निर्देशित संश्लेषण". Proceedings of Formal Methods in Computer-Aided Design. IEEE. p. 8.

[6] SyGuS-Comp (Syntax-Guided Synthesis Competition)

[7] Zohar Manna, Richard Waldinger (Jan 1980). "कार्यक्रम संश्लेषण के लिए एक निगमनात्मक दृष्टिकोण". ACM Transactions on Programming Languages and Systems. 2: 90–121. doi:10.1145/357084.357090. S2CID 14770735.

[8] Zohar Manna and Richard Waldinger (Dec 1978). कार्यक्रम संश्लेषण के लिए एक निगमनात्मक दृष्टिकोण (PDF) (Technical Note). SRI International. Archived (PDF) from the original on January 27, 2021.

[11] See Manna, Waldinger (1980), p.100 for correctness of the resolution rules.

[12] Boyer, Robert S.; Moore, J. Strother (May 1983). शुद्ध लिस्प की ट्यूरिंग पूर्णता का एक यांत्रिक प्रमाण (PDF) (Technical report). Institute for Computing Science, University of Texas at Austin. 37. Archived (PDF) from the original on 22 September 2017.

[14] Manna, Waldinger (1980), p.108-111

[15] Zohar Manna and Richard Waldinger (Aug 1987). "एक द्विआधारी-खोज प्रतिमान की उत्पत्ति". Science of Computer Programming. 9 (1): 37–83. doi:10.1016/0167-6423(87)90025-6.

[16] Daniele Nardi (1989). "निगमनात्मक-झांकी विधि द्वारा एक एकीकरण एल्गोरिथम का औपचारिक संश्लेषण". Journal of Logic Programming. 7: 1–43. doi:10.1016/0743-1066(89)90008-3.

[17] Daniele Nardi and Riccardo Rosati (1992). "Deductive Synthesis of Programs for Query Answering". In Kung-Kiu Lau and Tim Clement (ed.). तर्क कार्यक्रम संश्लेषण और परिवर्तन पर अंतर्राष्ट्रीय कार्यशाला (LOPSTR). Workshops in Computing. Springer. pp. 15–29. doi:10.1007/978-1-4471-3560-9_2.

[18] Jonathan Traugott (1986). "Deductive Synthesis of Sorting Programs". स्वचालित कटौती पर अंतर्राष्ट्रीय सम्मेलन की कार्यवाही. LNCS. Vol. 230. Springer. pp. 641–660.

[19] Jonathan Traugott (Jun 1989). "छँटाई कार्यक्रमों का निगमनात्मक संश्लेषण". Journal of Symbolic Computation. 7 (6): 533–572. doi:10.1016/S0747-7171(89)80040-9.

[20] Manna, Waldinger (1980), p.99

[21] Manna, Waldinger (1980), p.104

[22] Manna, Waldinger (1980), p.103, referring to: Neil V. Murray (Feb 1979). A Proof Procedure for Quantifier-Free Non-Clausal First Order Logic (Technical report). Syracuse Univ. 2-79.

[23] Zohar Manna, Richard Waldinger (Jan 1986). "स्वचालित कटौती में विशेष संबंध". Journal of the ACM. 33: 1–59. doi:10.1145/4904.4905. S2CID 15140138.

[24] Zohar Manna, Richard Waldinger (1992). "The Special-Relations Rules are Incomplete". प्रक्रिया। सीएडीई 11. LNCS. Vol. 607. Springer. pp. 492–506.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[note 1]

[note 2]

[9]

[10]

[note 3]

[11]

[12]

[13]

[14]

[15]

[16]

[17]

[18]

[19]

[20]

[21]

[note 4]

[note 5]

@@ Line 1: / Line 1: @@
-[[कंप्यूटर विज्ञान]] में, प्रोग्राम सिंथेसिस एक ऐसा [[कंप्यूटर प्रोग्राम]] बनाने का कार्य है जो उपयुक्त रूप से सही हो{{sic|hide=y}} दिए गए उच्च-स्तरीय [[औपचारिक विनिर्देश]] को संतुष्ट करता है। [[कार्यक्रम सत्यापन]] के विपरीत, कार्यक्रम दिए जाने के बजाय निर्मित किया जाना है; हालाँकि, दोनों क्षेत्र औपचारिक प्रूफ तकनीकों का उपयोग करते हैं, और दोनों में स्वचालितकरण की विभिन्न डिग्री के दृष्टिकोण शामिल हैं। [[स्वचालित प्रोग्रामिंग]] तकनीकों के विपरीत, प्रोग्राम संश्लेषण में विनिर्देश आमतौर पर उपयुक्त [[औपचारिक प्रणाली]] में गैर-एल्गोरिदमिक कथन होते हैं।<ref>{{cite book |last1= Basin |first1= D. |last2= Deville |first2= Y. |last3= Flener |first3 = P. |last4= Hamfelt |first4= A. |last5= Fischer Nilsson |first5= J. |chapter= Synthesis of programs in computational logic |editor=M. Bruynooghe and K.-K. Lau | publisher=Springer | series=LNCS | volume=3049 | pages=30&ndash;65 |citeseerx=10.1.1.62.4976 |title= कम्प्यूटेशनल लॉजिक में प्रोग्राम डेवलपमेंट| year = 2004 }}</ref>
+[[कंप्यूटर विज्ञान]] में, प्रोग्राम सिंथेसिस एक ऐसा कार्यक्रम बनाने का कार्य है किसी दिए गए उच्च-स्तरीय औपचारिक विनिर्देश को प्रमाणित करता है। [[कार्यक्रम सत्यापन]] के विपरीत, कार्यक्रम दिए जाने के बजाय निर्मित किया जाना है; तथापि, दोनों क्षेत्र औपचारिक प्रमाण तकनीकों का उपयोग करते हैं, और दोनों में स्वचालितकरण की विभिन्न डिग्री के दृष्टिकोण सम्मिलित हैं। [[स्वचालित प्रोग्रामिंग]] तकनीकों के विपरीत, प्रोग्राम सिंथेसिस में विनिर्देश सामान्यतः एक उपयुक्त तार्किक कलन में गैर-एल्गोरिदमिक कथन होते हैं।<ref>{{cite book |last1= Basin |first1= D. |last2= Deville |first2= Y. |last3= Flener |first3 = P. |last4= Hamfelt |first4= A. |last5= Fischer Nilsson |first5= J. |chapter= Synthesis of programs in computational logic |editor=M. Bruynooghe and K.-K. Lau | publisher=Springer | series=LNCS | volume=3049 | pages=30&ndash;65 |citeseerx=10.1.1.62.4976 |title= कम्प्यूटेशनल लॉजिक में प्रोग्राम डेवलपमेंट| year = 2004 }}</ref>
 == उत्पत्ति ==
-में कॉर्नेल विश्वविद्यालय में समर इंस्टीट्यूट ऑफ सिंबॉलिक लॉजिक के दौरान, [[अलोंजो चर्च]] ने गणितीय आवश्यकताओं से एक सर्किट को संश्लेषित करने की समस्या को परिभाषित किया।<ref>{{cite journal| author=Alonzo Church| title=परिपथ संश्लेषण की समस्या के लिए पुनरावर्ती अंकगणित के अनुप्रयोग| journal=Summaries of the Summer Institute of Symbolic Logic|date=1957| volume=1| pages=3–50}}</ref> भले ही काम केवल सर्किट को संदर्भित करता है और प्रोग्राम को नहीं, काम को प्रोग्राम सिंथेसिस के शुरुआती विवरणों में से एक माना जाता है और कुछ शोधकर्ता प्रोग्राम सिंथेसिस को चर्च की समस्या के रूप में संदर्भित करते हैं। 1960 के दशक में, आर्टिफिशियल इंटेलिजेंस में शोधकर्ताओं द्वारा एक स्वचालित प्रोग्रामर के लिए इसी तरह के विचार की खोज की गई थी।{{Citation needed|date=June 2010}}
+में कॉर्नेल विश्वविद्यालय में समर इंस्टीट्यूट ऑफ सिंबॉलिक लॉजिक के दौरान, [[अलोंजो चर्च]] ने गणितीय आवश्यकताओं से एक सर्किट को संश्लेषित करने की समस्या को परिभाषित किया।<ref>{{cite journal| author=Alonzo Church| title=परिपथ संश्लेषण की समस्या के लिए पुनरावर्ती अंकगणित के अनुप्रयोग| journal=Summaries of the Summer Institute of Symbolic Logic|date=1957| volume=1| pages=3–50}}</ref> भले ही काम केवल सर्किट को संदर्भित करता है और कार्यक्रम को नहीं, काम को प्रोग्राम सिंथेसिस के प्रारंभिक विवरणों में से एक माना जाता है और कुछ शोधकर्ता प्रोग्राम सिंथेसिस को "चर्च की समस्या" के रूप में संदर्भित करते हैं। 1960 के दशक में, आर्टिफिशियल इंटेलिजेंस में शोधकर्ताओं द्वारा "स्वचालित प्रोग्रामर" के लिए एक समान विचार की खोज की गई थी।{{Citation needed|date=June 2010}}
-तब से, विभिन्न अनुसंधान समुदायों ने कार्यक्रम संश्लेषण की समस्या पर विचार किया। उल्लेखनीय कार्यों में जूलियस रिचर्ड बुच्ची द्वारा 1969 का ऑटोमेटा-सैद्धांतिक दृष्टिकोण शामिल है। बुच्ची और [[लॉरेंस लैंडवेबर]],<ref>{{cite journal| author=Richard Büchi, Lawrence Landweber| title=परिमित-राज्य रणनीतियों द्वारा अनुक्रमिक स्थितियों को हल करना| journal=Transactions of the American Mathematical Society|date=Apr 1969| volume=138| pages=295–311| doi=10.2307/1994916| url=http://docs.lib.purdue.edu/cgi/viewcontent.cgi?article=1087&context=cstech| jstor=1994916}}</ref> और [[ जौहर मन्ना ]] और [[रिचर्ड वाल्डिंगर]] (सी। 1980) द्वारा काम करता है। आधुनिक उच्च-स्तरीय प्रोग्रामिंग भाषाओं के विकास को प्रोग्राम सिंथेसिस के एक रूप के रूप में भी समझा जा सकता है।
+तब से, विभिन्न अनुसंधान समुदायों ने प्रोग्राम सिंथेसिस की समस्या पर विचार किया। उल्लेखनीय कार्यों में बुच्ची और लैंडवेबर द्वारा 1969 ऑटोमेटा-सैद्धांतिक दृष्टिकोण,<ref>{{cite journal| author=Richard Büchi, Lawrence Landweber| title=परिमित-राज्य रणनीतियों द्वारा अनुक्रमिक स्थितियों को हल करना| journal=Transactions of the American Mathematical Society|date=Apr 1969| volume=138| pages=295–311| doi=10.2307/1994916| url=http://docs.lib.purdue.edu/cgi/viewcontent.cgi?article=1087&context=cstech| jstor=1994916}}</ref> और मन्ना और वाल्डिंगर (सी। 1980) द्वारा कार्य सम्मिलित हैं। आधुनिक उच्च-स्तरीय प्रोग्रामिंग भाषाओं के विकास को प्रोग्राम सिंथेसिस के एक रूप के रूप में भी समझा जा सकता है।
-== 21वीं सदी के विकास ==
+== 21वीं सदी के घटनाक्रम ==
-{{expand section|with=a more detailed overview of contemporary approaches|date=December 2022}}
+वीं सदी के प्रारंभ में [[औपचारिक सत्यापन]] समुदाय और संबंधित क्षेत्रों में प्रोग्राम सिंथेसिस के विचार में व्यावहारिक रुचि में वृद्धि देखी गई है। अरमांडो सोलर-लेज़ामा ने दिखाया कि [[ बूलियन तर्क |बूलियन तर्क]] में प्रोग्राम सिंथेसिस समस्याओं को एनकोड करना संभव है और [[बूलियन संतुष्टि समस्या]] के लिए एल्गोरिदम का उपयोग स्वचालित रूप से कार्यक्रम खोजने के लिए किया जाता है।<ref>{{cite thesis |last=Solar-Lezama |first=Armando |date=2008 |title=स्केचिंग द्वारा प्रोग्राम संश्लेषण|type=Ph.D. |publisher=University of California, Berkeley |url=https://people.csail.mit.edu/asolar/papers/thesis.pdf}}</ref> 2013 में, [[UPenn|यूपीएन]], यूसी बर्कले और [[MIT|एमआईटी]] के शोधकर्ताओं द्वारा प्रोग्राम सिंथेसिस समस्याओं के लिए एक एकीकृत रूपरेखा प्रस्तावित की गई थी।<ref>{{cite conference |title =सिंटेक्स-निर्देशित संश्लेषण|last1 = Alur |first1 = Rajeev| last2 = al.| first2 = et| date = 2013| publisher = IEEE| book-title = Proceedings of Formal Methods in Computer-Aided Design| pages = 8}}</ref> 2014 के बाद से एक प्रतिस्पर्धी कार्यक्रम, सिंटैक्स-गाइडेड संश्लेषण प्रतियोगिता या एसयगस-कॉमपी में प्रोग्राम सिंथेसिस के लिए विभिन्न एल्गोरिदम की तुलना करने वाली एक वार्षिक प्रोग्राम सिंथेसिस प्रतियोगिता हुई है।<ref>[https://sygus.org/ SyGuS-Comp (Syntax-Guided Synthesis Competition)]</ref> फिर भी, उपलब्ध एल्गोरिदम केवल छोटे प्रोग्रामों को संश्लेषित करने में सक्षम हैं।
-वीं सदी की शुरुआत में [[औपचारिक सत्यापन]] समुदाय और संबंधित क्षेत्रों में कार्यक्रम संश्लेषण के विचार में व्यावहारिक रुचि में वृद्धि देखी गई है। अरमांडो सोलर-लेज़ामा ने दिखाया कि [[ बूलियन तर्क ]] में प्रोग्राम सिंथेसिस समस्याओं को एनकोड करना संभव है और [[बूलियन संतुष्टि समस्या]] के लिए एल्गोरिदम का उपयोग स्वचालित रूप से प्रोग्राम खोजने के लिए किया जाता है।<ref>{{cite thesis |last=Solar-Lezama |first=Armando |date=2008 |title=स्केचिंग द्वारा प्रोग्राम संश्लेषण|type=Ph.D. |publisher=University of California, Berkeley |url=https://people.csail.mit.edu/asolar/papers/thesis.pdf}}</ref> 2013 में, [[UPenn]], UC बर्कले और [[MIT]] के शोधकर्ताओं द्वारा कार्यक्रम संश्लेषण समस्याओं के लिए एक एकीकृत रूपरेखा प्रस्तावित की गई थी।<ref>{{cite conference |title =सिंटेक्स-निर्देशित संश्लेषण|last1 = Alur |first1 = Rajeev| last2 = al.| first2 = et| date = 2013| publisher = IEEE| book-title = Proceedings of Formal Methods in Computer-Aided Design| pages = 8}}</ref> 2014 के बाद से एक प्रतिस्पर्धी कार्यक्रम, सिंटैक्स-गाइडेड सिंथेसिस प्रतियोगिता या SyGuS-Comp में प्रोग्राम सिंथेसिस के लिए विभिन्न एल्गोरिदम की तुलना करते हुए एक वार्षिक प्रोग्राम सिंथेसिस प्रतियोगिता हुई है।<ref>[https://sygus.org/ SyGuS-Comp (Syntax-Guided Synthesis Competition)]</ref> फिर भी, उपलब्ध एल्गोरिदम केवल छोटे प्रोग्रामों को संश्लेषित करने में सक्षम हैं।
 == मन्ना और वाल्डिंगर की रूपरेखा ==
 {| class="wikitable" style="float:right;"
-|+ Non-clausal resolution rules (unifying substitutions not shown)
+|+ गैर-क्लॉज़ल रिज़ॉल्यूशन नियम (एकीकृत प्रतिस्थापन नहीं दिखाए गए)
 |-
-! Nr !! Assertions !! Goals !! Program !! Origin
+! एनआर !! अभिकथन !! लक्ष्य !! कार्यक्रम !! मूल
 |-
 | 51 || <math>E[p]</math> || ||  ||
@@ Line 25: / Line 24: @@
 | 54 || || <math>H[p]</math> || t ||
 |-
-| 55 || <math>E[\text{true}] \lor F[\text{false}]</math>||  ||  || Resolve(51,52)
+| 55 || <math>E[\text{true}] \lor F[\text{false}]</math>||  ||  || संकल्प(51,52)
 |-
-| 56 || || <math>\lnot F[\text{true}] \land G[\text{false}]</math> ||  s || Resolve(52,53)
+| 56 || || <math>\lnot F[\text{true}] \land G[\text{false}]</math> ||  s || संकल्प(52,53)
 |-
-| 57 || || <math>\lnot F[\text{false}] \land G[\text{true}]</math> ||  s  || Resolve(53,52)
+| 57 || || <math>\lnot F[\text{false}] \land G[\text{true}]</math> ||  s  || संकल्प(53,52)
 |-
-| 58 || || <math>G[\text{true}] \land H[\text{false}]</math> || p [[?:|?]] s [[?:|:]] t || Resolve(53,54)
+| 58 || || <math>G[\text{true}] \land H[\text{false}]</math> || p [[?:|?]] s [[?:|:]] t || संकल्प(53,54)
 |}
-में प्रकाशित ज़ोहर मन्ना और रिचर्ड वाल्डिंगर की रूपरेखा,<ref>{{cite journal| author=Zohar Manna, Richard Waldinger| title=कार्यक्रम संश्लेषण के लिए एक निगमनात्मक दृष्टिकोण| journal=ACM Transactions on Programming Languages and Systems|date=Jan 1980| volume=2| pages=90–121| doi=10.1145/357084.357090| s2cid=14770735}}</ref><ref>{{cite report | url=https://apps.dtic.mil/dtic/tr/fulltext/u2/a065558.pdf| archive-url=https://web.archive.org/web/20210127052044/https://apps.dtic.mil/dtic/tr/fulltext/u2/a065558.pdf| url-status=live| archive-date=January 27, 2021<!---http://www.sri.com/sites/default/files/uploads/publications/pdf/725.pdf---> | author=Zohar Manna and Richard Waldinger | title=कार्यक्रम संश्लेषण के लिए एक निगमनात्मक दृष्टिकोण| institution=SRI International | type=Technical Note | number=177 | date=Dec 1978 }}</ref> उपयोगकर्ता द्वारा दिए गए प्रथम-क्रम तर्क | प्रथम-क्रम विनिर्देश सूत्र से शुरू होता है। उस सूत्र के लिए, एक प्रमाण का निर्माण किया जाता है, जिससे एकीकरण (कंप्यूटर विज्ञान) से एक [[कार्यात्मक कार्यक्रम]] का संश्लेषण भी होता है # प्रथम-क्रम के शब्दों के प्रतिस्थापन का वाक्यात्मक एकीकरण।
+में प्रकाशित मन्ना और वाल्डिंगर का ढांचा,<ref>{{cite journal| author=Zohar Manna, Richard Waldinger| title=कार्यक्रम संश्लेषण के लिए एक निगमनात्मक दृष्टिकोण| journal=ACM Transactions on Programming Languages and Systems|date=Jan 1980| volume=2| pages=90–121| doi=10.1145/357084.357090| s2cid=14770735}}</ref><ref>{{cite report | url=https://apps.dtic.mil/dtic/tr/fulltext/u2/a065558.pdf| archive-url=https://web.archive.org/web/20210127052044/https://apps.dtic.mil/dtic/tr/fulltext/u2/a065558.pdf| url-status=live| archive-date=January 27, 2021<!---http://www.sri.com/sites/default/files/uploads/publications/pdf/725.pdf---> | author=Zohar Manna and Richard Waldinger | title=कार्यक्रम संश्लेषण के लिए एक निगमनात्मक दृष्टिकोण| institution=SRI International | type=Technical Note | number=177 | date=Dec 1978 }}</ref> उपयोगकर्ता द्वारा दिए गए पहले-क्रम विनिर्देश सूत्र से प्रारंभ होता है। उस सूत्र के लिए, एक प्रमाण का निर्माण किया जाता है, जिससे एक कार्यात्मक कार्यक्रम को एकीकृत प्रतिस्थापन से भी संश्लेषित किया जाता है।
-ढांचे को तालिका लेआउट में प्रस्तुत किया गया है, जिसमें कॉलम शामिल हैं:
+ढांचे को तालिका लेआउट में प्रस्तुत किया गया है, जिसमें कॉलम सम्मिलित हैं:
-* संदर्भ उद्देश्यों के लिए एक पंक्ति संख्या (Nr)।
+* संदर्भ उद्देश्यों के लिए एक पंक्ति संख्या ("एनआर")।
-* सुगठित सूत्र # विधेय तर्क जो पहले से ही स्थापित हो चुका है, जिसमें स्वयंसिद्ध और पूर्व शर्त शामिल हैं, (अभिकथन)
+* सूत्र जो पहले से ही स्थापित किए जा चुके हैं, जिनमें स्वयंसिद्ध और पूर्व शर्त सम्मिलित हैं, ("अभिकथन")
-* फॉर्मूले अभी भी साबित होने बाकी हैं, पोस्टकंडिशन सहित, (लक्ष्य),<ref group=note>The distinction "Assertions" / "Goals" is for convenience only; following the paradigm of [[proof by contradiction]], a Goal <math>F</math> is equivalent to an assertion <math> \lnot F</math>.</ref>
+* फॉर्मूले अभी भी सिद्ध होने बाकी हैं, पोस्टकंडिशन (लक्ष्य),<ref group="note">The distinction "Assertions" / "Goals" is for convenience only; following the paradigm of [[proof by contradiction]], a Goal <math>F</math> is equivalent to an assertion <math> \lnot F</math>.</ref> सम्मिलित हैं
-* टर्म (तर्क) एक वैध आउटपुट वैल्यू ( प्रोग्राम ) को दर्शाता है<ref group=note>When <math>F</math> and <math>s</math> is the Goal formula and the Program term in a line, respectively, then in all cases where <math>F</math> holds, <math>s</math> is a valid output of the program to be synthesized. This [[invariant (computer science)|invariant]] is maintained by all proof rules. An Assertion formula usually is not associated with a Program term.</ref>
+* वैध आउटपुट वैल्यू ("प्रोग्राम") को दर्शाने वाली शर्तें<ref group="note">When <math>F</math> and <math>s</math> is the Goal formula and the Program term in a line, respectively, then in all cases where <math>F</math> holds, <math>s</math> is a valid output of the program to be synthesized. This [[invariant (computer science)|invariant]] is maintained by all proof rules. An Assertion formula usually is not associated with a Program term.</ref>
-* वर्तमान लाइन के लिए एक औचित्य (उत्पत्ति)
+* वर्तमान पंक्ति के लिए एक औचित्य ("उत्पत्ति")
-प्रारंभ में, पृष्ठभूमि ज्ञान, पूर्व-शर्तें और पश्च-शर्तें तालिका में दर्ज की जाती हैं। उसके बाद, उपयुक्त प्रूफ नियम मैन्युअल रूप से लागू किए जाते हैं। ढांचे को मध्यवर्ती सूत्रों की मानव पठनीयता को बढ़ाने के लिए डिज़ाइन किया गया है: [[संकल्प (तर्क)]] के विपरीत, इसे [[क्लॉसल सामान्य रूप]] की आवश्यकता नहीं होती है, लेकिन मनमाना संरचना के सूत्रों के साथ तर्क करने की अनुमति देता है और किसी भी जंक्शनर्स ([[गैर-खंड संकल्प]]) को शामिल करता है। प्रमाण कब पूरा होता है <math>\it true</math> लक्ष्य कॉलम में प्राप्त किया गया है, या, समकक्ष, <math>\it false</math> अभिकथन कॉलम में। इस दृष्टिकोण से प्राप्त कार्यक्रम से शुरू होने वाले विनिर्देश सूत्र को पूरा करने की गारंटी है; इस अर्थ में वे निर्माण द्वारा सही हैं।<ref>See Manna, Waldinger (1980), p.100 for correctness of the resolution rules.</ref> केवल एक न्यूनतावादी, फिर भी [[ट्यूरिंग-पूर्ण]],<ref>{{cite techreport |last1=Boyer |first1=Robert S. |last2=Moore |first2=J. Strother |title=शुद्ध लिस्प की ट्यूरिंग पूर्णता का एक यांत्रिक प्रमाण|number=37 |institution=Institute for Computing Science, University of Texas at Austin |date=May 1983 |url=http://www.cs.utexas.edu/users/boyer/ftp/ics-reports/cmp37.pdf |format=PDF |url-status=live |archive-date=22 September 2017 |archive-url=https://web.archive.org/web/20170922044624/http://www.cs.utexas.edu/users/boyer/ftp/ics-reports/cmp37.pdf |df=dmy-all }}</ref> [[विशुद्ध रूप से कार्यात्मक प्रोग्रामिंग भाषा]], जिसमें सशर्त, पुनरावर्तन और अंकगणित और अन्य ऑपरेटर शामिल हैं<ref group=note>Only the conditional operator ([[?:]]) is supported from the beginning. However, arbitrary new operators and relations can be added by providing their properties as axioms. In the toy example below, only the properties of <math>=</math> and <math>\leq</math> that are actually needed in the proof have been axiomatized, in line 1 to 3.</ref> समर्थित है।
+प्रारंभ में, पृष्ठभूमि ज्ञान, पूर्व-शर्तें और पश्च-शर्तें तालिका में दर्ज की जाती हैं। उसके बाद, उपयुक्त प्रमाण नियम मैन्युअल रूप से लागू किए जाते हैं। ढांचे को मध्यवर्ती सूत्रों की मानव पठनीयता को बढ़ाने के लिए डिज़ाइन किया गया है: शास्त्रीय[[संकल्प (तर्क)|संकल्प]] के विपरीत, इसे [[क्लॉसल सामान्य रूप]] की आवश्यकता नहीं होती है, लेकिन मनमाना संरचना के सूत्रों के साथ तर्क करने की अनुमति देता है और किसी भी जंक्शनर्स ("[[गैर-खंड संकल्प]]") को सम्मिलित करता है। प्रमाण कब पूरा होता है <math>\it true</math> लक्ष्य स्तंभ में व्युत्पन्न किया गया है, या, समकक्ष रूप से, <math>\it false</math> अभिकथन कॉलम में। इस दृष्टिकोण से प्राप्त कार्यक्रम से प्रारंभ होने वाले विनिर्देश सूत्र को पूरा करने की गारंटी है; इस अर्थ में वे निर्माण द्वारा सही हैं।<ref>See Manna, Waldinger (1980), p.100 for correctness of the resolution rules.</ref> केवल एक न्यूनतावादी, अभी तक [[ट्यूरिंग-पूर्ण]],<ref>{{cite techreport |last1=Boyer |first1=Robert S. |last2=Moore |first2=J. Strother |title=शुद्ध लिस्प की ट्यूरिंग पूर्णता का एक यांत्रिक प्रमाण|number=37 |institution=Institute for Computing Science, University of Texas at Austin |date=May 1983 |url=http://www.cs.utexas.edu/users/boyer/ftp/ics-reports/cmp37.pdf |format=PDF |url-status=live |archive-date=22 September 2017 |archive-url=https://web.archive.org/web/20170922044624/http://www.cs.utexas.edu/users/boyer/ftp/ics-reports/cmp37.pdf |df=dmy-all }}</ref> [[विशुद्ध रूप से कार्यात्मक प्रोग्रामिंग भाषा]], जिसमें सशर्त, पुनरावर्तन और अंकगणित और अन्य ऑपरेटर सम्मिलित हैं<ref group="note">Only the conditional operator ([[?:]]) is supported from the beginning. However, arbitrary new operators and relations can be added by providing their properties as axioms. In the toy example below, only the properties of <math>=</math> and <math>\leq</math> that are actually needed in the proof have been axiomatized, in line 1 to 3.</ref> समर्थित है।
-इस ढांचे के भीतर किए गए मामले के अध्ययन ने गणना करने के लिए एल्गोरिदम को संश्लेषित किया उदा। [[विभाजन एल्गोरिथ्म]], [[शेष]],<ref>Manna, Waldinger (1980), p.108-111</ref> [[वर्गमूल]],<ref>{{cite journal | author=Zohar Manna and Richard Waldinger | title=एक द्विआधारी-खोज प्रतिमान की उत्पत्ति| journal=Science of Computer Programming | volume=9 | number=1 | pages=37&ndash;83 | date=Aug 1987 | doi=10.1016/0167-6423(87)90025-6 | doi-access=free }}</ref> [[एकीकरण (कंप्यूटर विज्ञान)]],<ref>{{cite journal | author=Daniele Nardi | title=निगमनात्मक-झांकी विधि द्वारा एक एकीकरण एल्गोरिथम का औपचारिक संश्लेषण| journal=[[Journal of Logic Programming]] | volume=7 | pages=1&ndash;43 | year=1989 | doi=10.1016/0743-1066(89)90008-3 | doi-access=free }}</ref> संबंधपरक डेटाबेस प्रश्नों के उत्तर<ref>{{cite book | author=Daniele Nardi and Riccardo Rosati | contribution=Deductive Synthesis of Programs for Query Answering | editor=Kung-Kiu Lau and Tim Clement | title=तर्क कार्यक्रम संश्लेषण और परिवर्तन पर अंतर्राष्ट्रीय कार्यशाला (LOPSTR)| publisher=Springer | series=Workshops in Computing | pages=15&ndash;29 | year=1992 | doi=10.1007/978-1-4471-3560-9_2 }}</ref> और कई छँटाई एल्गोरिदम।<ref>{{cite book | author=Jonathan Traugott | contribution=Deductive Synthesis of Sorting Programs | title=स्वचालित कटौती पर अंतर्राष्ट्रीय सम्मेलन की कार्यवाही| publisher=Springer | series=[[LNCS]] | volume=230 | pages=641&ndash;660 | year=1986 }}</ref><ref>{{cite journal | author=Jonathan Traugott | title=छँटाई कार्यक्रमों का निगमनात्मक संश्लेषण| journal=[[Journal of Symbolic Computation]] | volume=7 | number=6 | pages=533&ndash;572 | date=Jun 1989 | doi=10.1016/S0747-7171(89)80040-9 | doi-access=free }}</ref>
+इस ढांचे के भीतर किए गए मामले के अध्ययन ने गणना करने के लिए एल्गोरिदम को संश्लेषित किया उदाहरण के लिए [[विभाजन एल्गोरिथ्म|विभाजन]], [[शेष]],<ref>Manna, Waldinger (1980), p.108-111</ref> [[वर्गमूल]],<ref>{{cite journal | author=Zohar Manna and Richard Waldinger | title=एक द्विआधारी-खोज प्रतिमान की उत्पत्ति| journal=Science of Computer Programming | volume=9 | number=1 | pages=37&ndash;83 | date=Aug 1987 | doi=10.1016/0167-6423(87)90025-6 | doi-access=free }}</ref> [[एकीकरण (कंप्यूटर विज्ञान)|एकीकरण]],<ref>{{cite journal | author=Daniele Nardi | title=निगमनात्मक-झांकी विधि द्वारा एक एकीकरण एल्गोरिथम का औपचारिक संश्लेषण| journal=[[Journal of Logic Programming]] | volume=7 | pages=1&ndash;43 | year=1989 | doi=10.1016/0743-1066(89)90008-3 | doi-access=free }}</ref> संबंधपरक डेटाबेस प्रश्नों के उत्तर<ref>{{cite book | author=Daniele Nardi and Riccardo Rosati | contribution=Deductive Synthesis of Programs for Query Answering | editor=Kung-Kiu Lau and Tim Clement | title=तर्क कार्यक्रम संश्लेषण और परिवर्तन पर अंतर्राष्ट्रीय कार्यशाला (LOPSTR)| publisher=Springer | series=Workshops in Computing | pages=15&ndash;29 | year=1992 | doi=10.1007/978-1-4471-3560-9_2 }}</ref> और कई छँटाई एल्गोरिदम।<ref>{{cite book | author=Jonathan Traugott | contribution=Deductive Synthesis of Sorting Programs | title=स्वचालित कटौती पर अंतर्राष्ट्रीय सम्मेलन की कार्यवाही| publisher=Springer | series=[[LNCS]] | volume=230 | pages=641&ndash;660 | year=1986 }}</ref><ref>{{cite journal | author=Jonathan Traugott | title=छँटाई कार्यक्रमों का निगमनात्मक संश्लेषण| journal=[[Journal of Symbolic Computation]] | volume=7 | number=6 | pages=533&ndash;572 | date=Jun 1989 | doi=10.1016/S0747-7171(89)80040-9 | doi-access=free }}</ref>
-=== सबूत नियम ===
+=== प्रमाण नियम ===
-प्रमाण नियमों में शामिल हैं:
+प्रमाण नियमों में सम्मिलित हैं:
-*नॉन-क्लॉज़ल रेज़ोल्यूशन (तर्क) (तालिका देखें)।
+*नॉन-क्लॉज़ल रेज़ोल्यूशन (तालिका देखें)।
-: उदाहरण के लिए, अभिकथन सूत्रों को हल करके पंक्ति 55 प्राप्त की जाती है <math>E</math> 51 से और <math>F</math> 52 से जो दोनों कुछ सामान्य उपसूत्र साझा करते हैं <math>p</math>. विलायक के विघटन के रूप में बनता है <math>E</math>, साथ <math>p</math> द्वारा प्रतिस्थापित <math>\it true</math>, और <math>F</math>, साथ <math>p</math> द्वारा प्रतिस्थापित <math>\it false</math>. यह विलायक तार्किक रूप से के संयोजन से अनुसरण करता है <math>E</math> और <math>F</math>. आम तौर पर अधिक, <math>E</math> और <math>F</math> केवल दो अविवेकी उपसूत्रों की आवश्यकता है <math>p_1</math> और <math>p_2</math>, क्रमश; उनके विलायक तब से बनते हैं <math>E \theta</math> और <math>F \theta</math> पहले की तरह, कहाँ <math>\theta</math> का सबसे सामान्य एकीकरणकर्ता है <math>p_1</math> और <math>p_2</math>. यह नियम पहले क्रम के तर्क में संकल्प (तर्क) #संकल्प का सामान्यीकरण करता है।<ref>Manna, Waldinger (1980), p.99</ref>
+: उदाहरण के लिए, अभिकथन सूत्रों को हल करके पंक्ति 55 प्राप्त की जाती है <math>E</math> 51 से और <math>F</math> 52 से जो दोनों कुछ सामान्य उपसूत्र साझा करते हैं <math>p</math>. विलायक के विघटन के रूप में बनता है <math>E</math>, साथ <math>p</math> द्वारा प्रतिस्थापित किया गया <math>\it true</math>, और <math>F</math>, साथ <math>p</math> द्वारा प्रतिस्थापित किया गया <math>\it false</math>। यह विलायक तार्किक रूप से के संयोजन से अनुसरण करता है <math>E</math> और <math>F</math>। अधिक सामान्यतः, <math>E</math> और <math>F</math> को केवल दो अविवेकी उपसूत्रों की आवश्यकता है <math>p_1</math> और <math>p_2</math>, क्रमश; उनके विलायक तब से बनते हैं <math>E \theta</math> और <math>F \theta</math> पहले की तरह, जहाँ <math>\theta</math> का सबसे सामान्य एकीकृतकर्ता है <math>p_1</math>और <math>p_2</math>। यह नियम खंडों के समाधान का सामान्यीकरण करता है। <ref>Manna, Waldinger (1980), p.99</ref>
-:पैरेंट फ़ार्मुलों की प्रोग्राम शर्तों को संयोजित किया जाता है, जैसा कि पंक्ति 58 में दिखाया गया है ताकि रिज़ॉल्वेंट का आउटपुट तैयार किया जा सके। सामान्य मामले में, <math>\theta</math> बाद पर भी लागू होता है। सबफॉर्मूला के बाद से <math>p</math> आउटपुट में दिखाई देता है, गणना योग्य गुणों के अनुरूप केवल उप सूत्रों पर हल करने के लिए देखभाल की जानी चाहिए।
+:रिज़ॉल्वेंट के आउटपुट को बनाने के लिए पैरेंट फ़ार्मुलों के प्रोग्राम टर्म्स को लाइन 58 में दिखाए अनुसार संयोजित किया जाता है। सामान्य मामले में, <math>\theta</math> बाद वाले पर भी लागू होता है। सबफॉर्मूला के बाद से <math>p</math> आउटपुट में दिखाई देता है, गणना योग्य गुणों के अनुरूप केवल उप सूत्रों पर हल करने के लिए देखभाल की जानी चाहिए।
 * तार्किक परिवर्तन।
-:उदाहरण के लिए, <math>E \land (F \lor G)</math> में परिवर्तित किया जा सकता है <math>(E \land F) \lor (E \land G)</math>) अभिकथन के साथ-साथ लक्ष्यों में भी, क्योंकि दोनों समतुल्य हैं।
+:उदाहरण के लिए, <math>E \land (F \lor G)</math> को रूपांतरित किया जा सकता है <math>(E \land F) \lor (E \land G)</math>) अभिकथन और साथ ही लक्ष्यों में, क्योंकि दोनों समान हैं।
 * संयोजक अभिकथनों और वियोजनात्मक लक्ष्यों का विभाजन।
-: नीचे दिए गए खिलौने के उदाहरण की 11 से 13 पंक्तियों में एक उदाहरण दिखाया गया है।
+: एक उदाहरण नीचे दिए गए खिलौने के उदाहरण की 11 से 13 पंक्तियों में दिखाया गया है।
 * [[संरचनात्मक प्रेरण]]।
-: यह नियम [[पुनरावर्ती कार्य (प्रोग्रामिंग)]] के संश्लेषण की अनुमति देता है। दी गई पूर्व और पश्‍चात शर्त के लिए <math>x</math> ऐसा है कि <math>\textit{pre}(x)</math>, पाना <math>f(x) = y</math> ऐसा है कि <math>\textit{post}(x,y)</math>, और एक उपयुक्त उपयोगकर्ता द्वारा दिया गया [[सुव्यवस्थित]] आदेश <math>\prec</math> के डोमेन का <math>x</math>, एक अभिकथन जोड़ना हमेशा सही होता है<math>x' \prec x \land \textit{pre}(x') \implies \textit{post}(x',f(x'))</math>.<ref>Manna, Waldinger (1980), p.104</ref> इस अभिकथन के साथ समाधान करने के लिए एक पुनरावर्ती कॉल का परिचय दिया जा सकता है <math>f</math> कार्यक्रम अवधि में।
+: यह नियम [[पुनरावर्ती कार्य (प्रोग्रामिंग)|पुनरावर्ती कार्यों]] के संश्लेषण की अनुमति देता है। किसी दिए गए पूर्व और बाद की स्थिति के लिए "दिया गया <math>x</math> ऐसा है कि <math>\textit{pre}(x)</math>, ढूंढें <math>f(x) = y</math> ऐसा है कि <math>\textit{post}(x,y)</math>", और एक उपयुक्त उपयोगकर्ता द्वारा दिया गया [[सुव्यवस्थित]] आदेश <math>\prec</math> के डोमेन <math>x</math>, एक अभिकथन जोड़ना हमेशा अच्छा होता है<math>x' \prec x \land \textit{pre}(x') \implies \textit{post}(x',f(x'))</math>.<ref>Manna, Waldinger (1980), p.104</ref> इस अभिकथन के साथ समाधान करने के लिए एक पुनरावर्ती कॉल प्रस्तुत कर सकता है <math>f</math> कार्यक्रम अवधि में।
 : मन्ना, वाल्डिंगर (1980), पृष्ठ 108-111 में एक उदाहरण दिया गया है, जहां दो दिए गए पूर्णांकों के भागफल और शेष की गणना करने के लिए एक एल्गोरिथ्म को अच्छी तरह से क्रम का उपयोग करके संश्लेषित किया जाता है। <math>(n',d') \prec (n,d)</math> द्वारा परिभाषित <math>0 \leq n' < n</math> (पृष्ठ 110)।
-मुर्रे ने इन नियमों को प्रथम-क्रम तर्क के लिए [[पूर्णता (तर्क)]] के रूप में दिखाया है।<ref>Manna, Waldinger (1980), p.103, referring to: {{cite techreport| author=Neil V. Murray| title=A Proof Procedure for Quantifier-Free Non-Clausal First Order Logic|date=Feb 1979| number=2-79| institution=Syracuse Univ.| url=http://surface.syr.edu/cgi/viewcontent.cgi?article=1005&context=eecs_techreports}}</ref>
+मुर्रे ने इन नियमों को प्रथम-क्रम तर्क के लिए पूर्ण दिखाया है।<ref>Manna, Waldinger (1980), p.103, referring to: {{cite techreport| author=Neil V. Murray| title=A Proof Procedure for Quantifier-Free Non-Clausal First Order Logic|date=Feb 1979| number=2-79| institution=Syracuse Univ.| url=http://surface.syr.edu/cgi/viewcontent.cgi?article=1005&context=eecs_techreports}}</ref>
-में, मन्ना और वाल्डिंगर ने समानता को संभालने के लिए सामान्यीकृत ई-रिज़ॉल्यूशन और [[पैरामॉड्यूलेशन]] नियम जोड़े;<ref>{{cite journal| author=Zohar Manna, Richard Waldinger| title=स्वचालित कटौती में विशेष संबंध| journal=Journal of the ACM| volume=33|date=Jan 1986| pages=1–59|doi=10.1145/4904.4905 | s2cid=15140138| doi-access=free}}</ref> बाद में, ये नियम अधूरे निकले (लेकिन फिर भी सु[[दृढ़ता]])।<ref>{{cite book| author=Zohar Manna, Richard Waldinger| chapter=The Special-Relations Rules are Incomplete| title=प्रक्रिया। सीएडीई 11| year=1992| volume=607| pages=492–506| publisher=Springer| series=LNCS}}</ref>
+में, मन्ना और वाल्डिंगर ने समानता को संभालने के लिए सामान्यीकृत ई-रिज़ॉल्यूशन और [[पैरामॉड्यूलेशन]] नियम जोड़े;<ref>{{cite journal| author=Zohar Manna, Richard Waldinger| title=स्वचालित कटौती में विशेष संबंध| journal=Journal of the ACM| volume=33|date=Jan 1986| pages=1–59|doi=10.1145/4904.4905 | s2cid=15140138| doi-access=free}}</ref> बाद में, ये नियम अधूरे निकले (लेकिन फिर भी सही थे)।<ref>{{cite book| author=Zohar Manna, Richard Waldinger| chapter=The Special-Relations Rules are Incomplete| title=प्रक्रिया। सीएडीई 11| year=1992| volume=607| pages=492–506| publisher=Springer| series=LNCS}}</ref>
-{{clear}}
 === उदाहरण ===
 {| class="wikitable" style="float:right;"
-|+ Example synthesis of maximum function
+|+ अधिकतम कार्य का उदाहरण संश्लेषण
 |-
-! Nr !! Assertions !! Goals !! Program !! Origin
+! एनआर !! अभिकथन !! लक्ष्य !! कार्यक्रम !! मूल
 |-
-| 1 || <math>A=A</math> || ||  || Axiom
+| 1 || <math>A=A</math> || ||  || सिद्ध प्रमाण
 |-
-| 2 || <math>A \leq A</math>  ||  || || Axiom
+| 2 || <math>A \leq A</math>  ||  || || सिद्ध प्रमाण
 |-
-| 3 || <math>A \leq B \lor B \leq A</math>  || ||  || Axiom
+| 3 || <math>A \leq B \lor B \leq A</math>  || ||  || सिद्ध प्रमाण
 |-
-| 10 || || <math>x \leq M \land y \leq M \land (x = M \lor y = M)</math> || M || Specification
+| 10 || || <math>x \leq M \land y \leq M \land (x = M \lor y = M)</math> || M || विशेष विवरण
 |-
-| 11 || || <math>(x \leq M \land y \leq M \land x = M) \lor (x \leq M \land y \leq M \land y = M)</math> || M || Distr(10)
+| 11 || || <math>(x \leq M \land y \leq M \land x = M) \lor (x \leq M \land y \leq M \land y = M)</math> || M || डीआईएसटीआर(10)
 |-
-| 12 || || <math>x \leq M \land y \leq M \land x = M</math> || M || Split(11)
+| 12 || || <math>x \leq M \land y \leq M \land x = M</math> || M || विभाजित करना(11)
 |-
-| 13 || || <math>x \leq M \land y \leq M \land y = M</math> || M || Split(11)
+| 13 || || <math>x \leq M \land y \leq M \land y = M</math> || M || विभाजित करना(11)
 |-
-| 14 || || <math>x \leq x \land y \leq x</math> || x || Resolve(12,1)
+| 14 || || <math>x \leq x \land y \leq x</math> || x || संकल्प(12,1)
 |-
-| 15 || || <math>y \leq x</math> || x || Resolve(14,2)
+| 15 || || <math>y \leq x</math> || x || संकल्प(14,2)
 |-
-| 16 || || <math>\lnot (x \leq y)</math> || x || Resolve(15,3)
+| 16 || || <math>\lnot (x \leq y)</math> || x || संकल्प(15,3)
 |-
-| 17 || || <math>x \leq y \land y \leq y</math> || y || Resolve(13,1)
+| 17 || || <math>x \leq y \land y \leq y</math> || y || संकल्प(13,1)
 |-
-| 18 || || <math>x \leq y</math> || y || Resolve(17,2)
+| 18 || || <math>x \leq y</math> || y || संकल्प(17,2)
 |-
-| 19 || || <math>\textit{true}</math> || x<y [[?:|?]] y [[?:|:]] x || Resolve(18,16)
+| 19 || || <math>\textit{true}</math> || x<y [[?:|?]] y [[?:|:]] x || संकल्प(18,16)
 |}
-एक खिलौना उदाहरण के रूप में, अधिकतम गणना करने के लिए एक कार्यात्मक कार्यक्रम <math>M</math> दो नंबर का <math>x</math> और <math>y</math> निम्नानुसार व्युत्पन्न किया जा सकता है।{{citation needed|date=May 2016}}
+एक खिलौना उदाहरण के रूप में, अधिकतम गणना करने के लिए एक कार्यात्मक प्रोग्राम दो नंबर का <math>M</math> <math>x</math> और <math>y</math> को निम्नानुसार प्राप्त किया जा सकता है।{{citation needed|date=May 2016}}
-आवश्यकता विवरण से शुरू करते हुए अधिकतम किसी भी संख्या से बड़ा या उसके बराबर है, और दी गई संख्याओं में से एक है, प्रथम-क्रम सूत्र <math>\forall X \forall Y \exists M: X \leq M \land Y \leq M \land (X=M \lor Y=M)</math> इसके औपचारिक अनुवाद के रूप में प्राप्त किया जाता है। इस सूत्र को सिद्ध करना है। रिवर्स [[ विद्वता ]] द्वारा,<ref group=note>While ordinary Skolemization preserves satisfiability, reverse Skolemization, i.e. replacing universally quantified variables by functions, preserves validity.</ref> पंक्ति 10 में विनिर्देश प्राप्त किया गया है, क्रमशः एक चर और एक स्कोलेम स्थिरांक को दर्शाने वाला एक अपर- और लोअर-केस अक्षर।
+आवश्यकता विवरण से प्रारंभ करते हुए "अधिकतम किसी भी संख्या से बड़ा या उसके बराबर है, और दी गई संख्याओं में से एक है", प्रथम-क्रम सूत्र <math>\forall X \forall Y \exists M: X \leq M \land Y \leq M \land (X=M \lor Y=M)</math> इसके औपचारिक अनुवाद के रूप में प्राप्त किया जाता है। इस सूत्र को सिद्ध करना है। रिवर्स [[ विद्वता |विद्वता]] द्वारा,<ref group=note>While ordinary Skolemization preserves satisfiability, reverse Skolemization, i.e. replacing universally quantified variables by functions, preserves validity.</ref> पंक्ति 10 में विशेष विवरण प्राप्त किया गया है, क्रमशः एक चर और एक स्कोलेम स्थिरांक को दर्शाते हुए एक बड़े और छोटे अक्षर।
 पंक्ति 11 में वितरण नियम के लिए रूपांतरण नियम लागू करने के बाद, प्रमाण लक्ष्य एक संयोजन है, और इसलिए इसे दो मामलों में विभाजित किया जा सकता है, अर्थात। लाइन 12 और 13।
-पहले मामले की ओर मुड़ते हुए, पंक्ति 12 को पंक्ति 1 में स्वयंसिद्ध के साथ हल करने से प्रतिस्थापन (तर्क) होता है # कार्यक्रम चर का पहला-क्रम तर्क <math>M</math> पंक्ति 14 में। सहज रूप से, पंक्ति 12 का अंतिम संयोजन मूल्य निर्धारित करता है <math>M</math> इस मामले में लेना चाहिए। औपचारिक रूप से, उपरोक्त पंक्ति 57 में दिखाया गया गैर-खंड संकल्प नियम 12 और 1 पंक्तियों पर लागू होता है <!---Using {{math}} here to make the color template work--->
+पहले मामले की ओर मुड़ते हुए, पंक्ति 12 को पंक्ति 1 में सिद्ध प्रमाण के साथ हल करने से कार्यक्रम चर की तात्कालिकता होती है <math>M</math> पंक्ति 14 में। सहज रूप से, पंक्ति 12 का अंतिम संयोजन मूल्य निर्धारित करता है <math>M</math> इस मामले में लेना चाहिए। औपचारिक रूप से, उपरोक्त पंक्ति 57 में दिखाया गया गैर-खंड संकल्प नियम 12 और 1 पंक्तियों पर लागू होता है
-* {{color|#008000|{{math|p}}}} सामान्य उदाहरण होने के नाते {{color|#008000|{{math|1=x=x}}}} का {{color|#408000|{{math|1=A=A}}}} और {{color|#008040|{{math|1=x=M}}}}, वाक्य-विन्यास एकीकरण (कंप्यूटर विज्ञान) द्वारा प्राप्त # पहले-क्रम की शर्तों के बाद के सूत्रों का वाक्य-विन्यास एकीकरण,
+* {{color|#008000|{{math|p}}}} का {{color|#408000|{{math|1=A=A}}}} और {{color|#008040|{{math|1=x=M}}}} का सामान्य उदाहरण {{color|#008000|{{math|1=x=x}}}} है, जो बाद के सूत्रों को वाक्यगत रूप से एकीकृत करके प्राप्त किया गया है,
-* {{color|#800000|{{math|F[}}}}{{color|#008000|{{math|p}}}}{{color|#800000|{{math|]}}}} प्राणी {{color|#800000|{{math|''true'' ∧ }}}}{{color|#008000|{{math|1=x=x}}}}, प्रतिस्थापन (तर्क) से प्राप्त # प्रथम-क्रम तर्क पंक्ति 1 (संदर्भ बनाने के लिए उचित रूप से गद्देदार {{color|#800000|{{math|F[⋅]}}}} आस-पास {{color|#008000|{{math|p}}}} दृश्यमान), और
+* {{color|#800000|{{math|F[}}}}{{color|#008000|{{math|p}}}}{{color|#800000|{{math|]}}}} {{color|#800000|{{math|''true'' ∧ }}}}{{color|#008000|{{math|1=x=x}}}}, तात्कालिक पंक्ति 1 से प्राप्त किया गया है (उचित रूप से पैड किया गया है ताकि संदर्भ {{color|#800000|{{math|F[⋅]}}}} को {{color|#008000|{{math|p}}}} के आसपास दिखाई दे), और
-* {{color|#000080|{{math|G[}}}}{{color|#008000|{{math|p}}}}{{color|#000080|{{math|]}}}} प्राणी {{color|#000080|{{math|x ≤ x ∧ y ≤ x ∧ }}}}{{color|#008000|{{math|1=x = x}}}}, तात्कालिक रेखा 12 से प्राप्त,
+* {{color|#000080|{{math|G[}}}}{{color|#008000|{{math|p}}}}{{color|#000080|{{math|]}}}} {{color|#000080|{{math|x ≤ x ∧ y ≤ x ∧ }}}}{{color|#008000|{{math|1=x = x}}}}, होने के नाते, तत्काल रेखा 12 से प्राप्त किया गया है,
 उपज
 <math>\lnot (</math>{{color|#800000|{{math|''true'' ∧ }}}}{{color|#008000|{{math|''false''}}}}{{math|) ∧ (}}{{color|#000080|{{math|x ≤ x ∧ y ≤ x ∧ }}}}{{color|#008000|{{math|''true''}}}}<math>)</math>,
-जो सरल करता है <math>x \leq x \land y \leq x</math>.
+जो करने के लिए सरल करता है <math>x \leq x \land y \leq x</math>.
-इसी तरह, लाइन 14 से लाइन 15 और फिर लाइन 16 रेजोल्यूशन से मिलती है। साथ ही, दूसरा मामला, <math>x \leq M \land y \leq M \land y = M</math> लाइन 13 में, इसी तरह से संभाला जाता है, अंत में लाइन 18 की उपज होती है।
+इसी तरह, लाइन 14 से लाइन 15 और फिर लाइन 16 रेजोल्यूशन से मिलती है। साथ ही, दूसरा मामला, <math>x \leq M \land y \leq M \land y = M</math> लाइन 13 में, इसी तरह से संभाला जाता है, अंत में लाइन 18 देता है।
-अंतिम चरण में, दोनों स्थितियाँ (यानी पंक्तियाँ 16 और 18) जुड़ जाती हैं, पंक्ति 58 से संकल्प नियम का उपयोग करते हुए; उस नियम को लागू करने के लिए प्रारंभिक चरण 15→16 की आवश्यकता थी। सहज रूप से, लाइन 18 को मामले की तरह पढ़ा जा सकता है <math>x \leq y</math>, उत्पादन <math>y</math> मान्य है (मूल विनिर्देशन के संबंध में), जबकि पंक्ति 15 कहती है case <math>y \leq x</math>, उत्पादन <math>x</math> यह सही है; चरण 15→16 ने स्थापित किया कि दोनों मामले 16 और 18 पूरक हैं।<ref group=note>Axiom 3 was needed for that; in fact, if <math>\leq</math> wasn't a [[total order]], no maximum could be computed for uncomparable inputs <math>x,y</math>.</ref> चूँकि 16 और 18 दोनों पंक्तियाँ एक प्रोग्राम टर्म के साथ आती हैं, a ?: प्रोग्राम कॉलम में परिणाम देता है। लक्ष्य सूत्र के बाद से <math>\textit{true}</math> व्युत्पन्न किया गया है, प्रमाण किया गया है, और का कार्यक्रम स्तंभ<math>\textit{true}</math>लाइन में कार्यक्रम शामिल है।
+अंतिम चरण में, दोनों स्थितियाँ (यानी पंक्तियाँ 16 और 18) जुड़ जाती हैं, पंक्ति 58 से संकल्प नियम का उपयोग करते हुए; उस नियम को लागू करने के लिए प्रारंभिक चरण 15→16 की आवश्यकता थी। सहज रूप से, पंक्ति 18 को "मामले में" के रूप में पढ़ा जा सकता है <math>x \leq y</math>, उत्पादन <math>y</math> मान्य है; चरण 15→16 ने स्थापित किया कि दोनों मामले 16 और 18 पूरक हैं।<ref group="note">Axiom 3 was needed for that; in fact, if <math>\leq</math> wasn't a [[total order]], no maximum could be computed for uncomparable inputs <math>x,y</math>.</ref> चूँकि दोनों पंक्तियाँ 16 और 18 एक कार्यक्रम शब्द के साथ आती हैं, एक सशर्त अभिव्यक्ति का परिणाम प्रोग्राम कॉलम में होता है। लक्ष्य सूत्र के बाद से <math>\textit{true}</math> व्युत्पन्न किया गया है, प्रमाण दिया गया है, और का कार्यक्रम स्तंभ <math>\textit{true}</math> पंक्ति में कार्यक्रम है।
 == यह भी देखें ==
@@ Line 129: / Line 126: @@
 * {{cite journal| author=Zohar Manna, Richard Waldinger| title=Knowledge and Reasoning in Program Synthesis| journal=Artificial Intelligence| year=1975| volume=6| issue=2| pages=175–208| doi=10.1016/0004-3702(75)90008-9}}
-{{DEFAULTSORT:Program Synthesis}}[[Category: प्रोग्रामिंग प्रतिमान]]
+{{DEFAULTSORT:Program Synthesis}}
-[[Category: Machine Translated Page]]
+[[Category:All articles with unsourced statements|Program Synthesis]]
-[[Category:Created On 02/03/2023]]
+[[Category:Articles with unsourced statements from June 2010|Program Synthesis]]
+[[Category:Articles with unsourced statements from May 2016|Program Synthesis]]
+[[Category:Created On 02/03/2023|Program Synthesis]]
+[[Category:Machine Translated Page|Program Synthesis]]
+[[Category:Pages with script errors|Program Synthesis]]
+[[Category:Templates Vigyan Ready|Program Synthesis]]
+[[Category:प्रोग्रामिंग प्रतिमान|Program Synthesis]]

Anonymous

Search

प्रोग्राम सिंथेसिस: Difference between revisions

Namespaces

More

Page actions

Latest revision as of 16:08, 11 April 2023

Contents

उत्पत्ति

21वीं सदी के घटनाक्रम

मन्ना और वाल्डिंगर की रूपरेखा

प्रमाण नियम

उदाहरण

यह भी देखें

टिप्पणियाँ

संदर्भ

Navigation

Navigation

Wiki tools

Wiki tools

Anonymous

Search

प्रोग्राम सिंथेसिस: Difference between revisions

Latest revision as of 16:08, 11 April 2023

उत्पत्ति

21वीं सदी के घटनाक्रम

मन्ना और वाल्डिंगर की रूपरेखा

प्रमाण नियम

उदाहरण

यह भी देखें

टिप्पणियाँ

संदर्भ

Navigation

Wiki tools

Page tools

Other projects

Categories