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

Revision as of 21:29, 15 March 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]

उदाहरण

Example synthesis of maximum function
Nr	Assertions	Goals	Program	Origin
1	$A=A$			Axiom
2	$A\leq A$			Axiom
3	$A\leq B\lor B\leq A$			Axiom
10		$x\leq M\land y\leq M\land (x=M\lor y=M)$	M	Specification
11		$(x\leq M\land y\leq M\land x=M)\lor (x\leq M\land y\leq M\land y=M)$	M	Distr(10)
12		$x\leq M\land y\leq M\land x=M$	M	Split(11)
13		$x\leq M\land y\leq M\land y=M$	M	Split(11)
14		$x\leq x\land y\leq x$	x	Resolve(12,1)
15		$y\leq x$	x	Resolve(14,2)
16		$\lnot (x\leq y)$	x	Resolve(15,3)
17		$x\leq y\land y\leq y$	y	Resolve(13,1)
18		$x\leq y$	y	Resolve(17,2)
19		${\textit {true}}$	x<y ? y : x	Resolve(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$ सामान्य उदाहरण होने के नाते $x=x$ का $A=A$ और $x=M$ , वाक्य-विन्यास एकीकरण (कंप्यूटर विज्ञान) द्वारा प्राप्त # पहले-क्रम की शर्तों के बाद के सूत्रों का वाक्य-विन्यास एकीकरण,
$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 कहती है case $y\leq x$ , उत्पादन $x$ यह सही है; चरण 15→16 ने स्थापित किया कि दोनों मामले 16 और 18 पूरक हैं।^{[note 5]} चूँकि 16 और 18 दोनों पंक्तियाँ एक कार्यक्रमटर्म के साथ आती हैं, a ?: कार्यक्रमकॉलम में परिणाम देता है। लक्ष्य सूत्र के बाद से ${\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 44: / Line 44: @@
-=== सबूत नियम ===
+=== प्रमाण नियम ===
-प्रमाण नियमों में शामिल हैं:
+प्रमाण नियमों में सम्मिलित हैं:
-*नॉन-क्लॉज़ल रेज़ोल्यूशन (तर्क) (तालिका देखें)।
+*नॉन-क्लॉज़ल रेज़ोल्यूशन (तालिका देखें)।
-: उदाहरण के लिए, अभिकथन सूत्रों को हल करके पंक्ति 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 पंक्तियों में एक उदाहरण दिखाया गया है।

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

Revision as of 21:29, 15 March 2023

Contents