View source for प्रेस्बर्गर अंकगणित

{{Short description|Decidable first-order theory of the natural numbers with addition}}
'''प्रेस्बर्गर अंकगणित''' मुख्य रूप से [[प्रथम-क्रम विधेय]] का ऐसा कलन है। जिसमें संयोजन के साथ [[प्राकृतिक संख्या|प्राकृतिक संख्याओं]] का प्रथम-क्रम सिद्धांत, जिसका नाम मोजेज़ प्रेस्बर्गर के सम्मान में रखा गया है, जिन्होंने इसे 1929 में प्रस्तुत किया था। प्रेस्बर्गर के आधार पर अंकगणित के [[हस्ताक्षर (गणितीय तर्क)|हस्ताक्षर गणितीय तर्क]] में केवल संयोजन संचालन और समानता सम्मिलित है, इस प्रकार [[गुणन संक्रिया]] को पूर्ण रूप से छोड़ दिया गया है। जिसके कारण स्वयंसिद्धों में [[गणितीय प्रेरण]] की योजना को सम्मिलित किया गया है।

प्रेस्बर्गर अंकगणित के आधार पर [[पीनो अंकगणित]] की तुलना में बहुत कमजोर है, जिसमें जोड़ और [[गुणा]] दोनों प्रक्रियाएँ सम्मिलित की गई हैं। इस प्रकार पीनो अंकगणित के विपरीत, प्रेस्बर्गर अंकगणित निर्णायकता तार्किक है। इसका अर्थ यह है कि प्रेस्बर्गर अंकगणित की भाषा में किसी भी वाक्य के लिए कलनिक रूप से यह निर्धारित करना संभव है कि क्या वह वाक्य प्रेस्बर्गर अंकगणित के सिद्धांतों से प्रमाणित करने योग्य है। चूंकि, इस कलन विधि के कलन का एसिम्प्टोटिक रनिंग टाइम विश्लेषण कम से कम [[दोहरा घातीय कार्य]] है, जैसा कि {{harvtxt|फिश्चर|रेबिन|1974}} में दिखाया गया है।

==अवलोकन==
प्रेस्बर्गर अंकगणित की भाषा में स्थिरांक 0 और 1 और बाइनरी फ़ंक्शन + सम्मिलित है, जिसकी मुख्यतः जोड़ के रूप में व्याख्या किया गया है।

इस भाषा में, प्रेस्बर्गर अंकगणित के स्वयंसिद्ध निम्नलिखित के [[सार्वभौमिक समापन]] इस प्रकार हैं:
# ¬(0 = x + 1)
# x + 1 = y + 1 → x = y
# x + 0 = x
# x + (y + 1) = (x + y) + 1
# मान लीजिए P(x) मुक्त चर x और संभवतः अन्य मुक्त चर हैं, जिसके साथ प्रेस्बर्गर अंकगणित की भाषा में [[प्रथम-क्रम तर्क]] या प्रथम-क्रम सूत्र है। फिर निम्नलिखित सूत्र स्वयंसिद्ध है: 
#(P(0) ∧ ∀x(P(x) → P(x + 1))) → ∀y P(y)

(5) [[गणितीय प्रेरण]] की स्वयंसिद्ध स्कीमा को प्रदर्शित करता है, जो अनंत रूप से कई स्वयंसिद्धों का प्रतिनिधित्व करती है। इन्हें किसी भी सीमित संख्या में स्वयंसिद्धों द्वारा प्रतिस्थापित नहीं किया जा सकता है, अर्थात, प्रेस्बर्गर अंकगणित प्रथम-क्रम तर्क में अंतिम रूप से स्वयंसिद्ध नहीं है।{{sfn|Zoethout|2015|p=8|loc=Theorem 1.2.4.}}

प्रेस्बर्गर अंकगणित को प्रथम-क्रम तर्क मुख्य रूप से प्रथम-क्रम सिद्धांत, प्रारूप और प्राथमिक वर्ग या प्रथम-क्रम सिद्धांत के रूप में देखा जा सकता है, जिसमें समानता के साथ उपरोक्त सिद्धांतों के सभी परिणाम सम्मिलित हैं। इस प्रकार वैकल्पिक रूप से इसे उन वाक्यों के समुच्चय के रूप में परिभाषित किया जा सकता है जो तार्किक व्याख्या के आधार पर इच्छित व्याख्याओं में सत्य मान को प्रदर्शित करते हैं: इसके लिए स्थिरांक 0, 1 के साथ गैर-ऋणात्मक पूर्णांकों की संरचना और गैर-ऋणात्मक पूर्णांकों का योग भी सम्मिलित किया जाता हैं।

प्रेस्बर्गर अंकगणित को पूर्ण और निर्णय लेने योग्य बनाया गया है। इसलिए यह विभाज्यता या मौलिकता इसके लिए अधिक सामान्य रूप से चर के गुणन की ओर ले जाने वाली किसी भी संख्या अवधारणा को प्रदर्शित करता हैं, इस प्रकार की अवधारणाओं को औपचारिक रूप से नहीं देखा जा सकता है। चूंकि यह विभाज्यता के व्यक्तिगत उदाहरण तैयार कर सकता है, उदाहरण के लिए यह सभी x के लिए प्रमाणित होता है, यहाँ पर y मुख्यतः (y + y = x) ∨ (y + y + 1 = x) रूप में उपस्थित है। यह बताता है कि प्रत्येक संख्या या तो सम या विषम है।

==गुण==

मोजेज़ प्रेस्बर्गर ने प्रेस्बर्गर अंकगणित को सिद्ध किया:
* [[संगति प्रमाण]]: प्रेस्बर्गर अंकगणित में ऐसा कोई कथन नहीं है जिसे स्वयंसिद्धों से इस प्रकार निकाला जा सके कि उसका निषेध भी निकाला जा सके।
* [[पूर्णता (तर्क)]]: प्रेस्बर्गर अंकगणित की भाषा में प्रत्येक कथन के लिए, या तो इसे स्वयंसिद्धों से निकालना संभव है या इसका निषेध निकालना संभव है।
* निर्णयशीलता (तर्क): [[कलन विधि]] उपस्थित है जो यह तय करता है कि प्रेस्बर्गर अंकगणित में दिया गया कोई भी कथन प्रमेय है या गैर-प्रमेय है।

प्रेस्बर्गर अंकगणित की निर्णायकता को अंकगणितीय सर्वांगसमता के बारे में तर्क द्वारा पूरक, क्वांटिफायर उन्मूलन का उपयोग करके दिखाया जा सकता है।{{sfn|Presburger|1929}}{{sfn|Monk|2012|p=240}}{{sfn|Nipkow|2010}}{{sfn|Enderton|2001|p=188}} इस प्रकार यहाँ पर क्वांटिफ़ायर एलिमिनेशन कलन को उचित ठहराने के लिए उपयोग किए जाने वाले चरणों का उपयोग पुनरावर्ती स्वयंसिद्धीकरणों को परिभाषित करने के लिए किया जा सकता है, जिनमें आवश्यक रूप से प्रेरण की स्वयंसिद्ध स्कीमा सम्मिलित नहीं होती है।{{sfn|Presburger|1929}}{{sfn|Stansifer|1984}}

इसके विपरीत, पीनो अंकगणित, जो कि गुणन के साथ संवर्धित प्रेस्बर्गर अंकगणित है, [[निर्णय समस्या]] के ऋणात्मक उत्तर के परिणामस्वरूप निर्णय लेने योग्य नहीं है। इस प्रकार गोडेल की अपूर्णता प्रमेय के अनुसार, पीनो अंकगणित अधूरा है और इसकी स्थिरता आंतरिक रूप से सिद्ध करने योग्य नहीं है, अपितु जेंटज़ेन की स्थिरता प्रमाण देखें।

=== कम्प्यूटरीकृत जटिलता ===
प्रेस्बर्गर अंकगणित के लिए निर्णय समस्या [[कम्प्यूटेशनल जटिलता सिद्धांत|कम्प्यूटरीकृत जटिलता सिद्धांत]] और [[गणना]] में उत्तम उदाहरण है। मान लीजिए कि प्रेस्बर्गर अंकगणित में कथन की लंबाई n है। इसके आधार पर {{harvtxt|फिश्चर|रेबिन|1974}} द्वारा प्रमाणित हुआ कि, इसकी सबसे बुरी स्थिति में पहले क्रम के तर्क में कथन के प्रमाण की लंबाई कम से कम <math>2^{2^{cn}}</math> होती है, इसके आधार पर कुछ स्थिरांक c>0 के लिए इसका मान दिया गया हैं। इसलिए प्रेस्बर्गर अंकगणित के लिए उनके निर्णय कलन का रनटाइम कम से कम घातीय है। फिशर और राबिन ने यह भी प्रमाणित किया कि किसी भी उचित स्वयंसिद्धीकरण को उनके पेपर में सटीक रूप से परिभाषित करने के लिए, लंबाई n के प्रमेय उपस्थित हैं जिनमें दोहरे घातीय फ़ंक्शन लंबाई प्रमाण हैं। इस प्रकार सहजता से इससे पता चलता है कि कंप्यूटर प्रोग्राम द्वारा क्या सिद्ध किया जा सकता है, इसकी कम्प्यूटरीकृत सीमाएँ हैं। इस प्रकार फिशर और राबिन के काम का यह भी तात्पर्य है कि प्रेस्बर्गर अंकगणित का उपयोग उन सूत्रों को परिभाषित करने के लिए किया जा सकता है जो किसी भी कलन की सही गणना करते हैं जब तक कि इनपुट अपेक्षाकृत बड़ी सीमा से कम न हो। इस प्रकार इसकी सीमाएँ बढ़ाई जा सकती हैं, अपितु इसके लिए उपयुक्त सूत्र का उपयोग किया जाता हैं। दूसरी ओर प्रेस्बर्गर अंकगणित के लिए निर्णय प्रक्रिया पर त्रिगुण घातीय ऊपरी सीमा {{harvtxt|ओपेन्न|1978}} द्वारा सिद्ध की गई थी।

वैकल्पिक जटिलता वर्गों का उपयोग करके अधिक सख्त जटिलता सीमा दिखाई गई थी {{harvtxt|Berman|1980}}. प्रेस्बर्गर अंकगणित (पीए) में सत्य कथनों का समुच्चय [[ वैकल्पिक ट्यूरिंग मशीन |वैकल्पिक ट्यूरिंग मशीन]] (2)<sup>2<sup>n</sup>O(1), n)</sup> के लिए पूरा दिखाया गया है, इस प्रकार इसकी जटिलता दोहरे घातीय गैर-नियतात्मक समय (2-NEXP) और दोहरे घातीय स्थान (2-एक्सस्पेस) के बीच है। इसके पूर्ण बहुपद समय पर इसके अनेक एक से एक कटौतियों के अंतर्गत प्रदर्शित होते है। यह भी ध्यान दें कि प्रेस्बर्गर अंकगणित को सामान्यतः पीए के रूप में संक्षिप्त किया जाता है, गणित में सामान्य तौर पर पीए का अर्थ सामान्यतः पीनो अंकगणित होता है।

अधिक सुक्ष्म परिणाम के लिए, मान लें कि PA(i) सत्य Σ<sub>i</sub> का समुच्चय है, यहाँ पर PA कथन, और PA(i, j) सत्य Σ<sub>i</sub> का समुच्चय प्रत्येक क्वांटिफायर ब्लॉक के साथ पीए स्टेटमेंट जे वेरिएबल्स तक सीमित हैं। इस प्रकार '<' को क्वांटिफायर-मुक्त माना जाता है, यहां, परिबद्ध परिमाणकों को परिमाणकों के रूप में गिना जाता है।<br/>PA(1, j) P में है, जबकि PA(1) NP-पूर्ण है।{{sfn|Nguyen Luu|2018|loc=chapter 3}}<br/>i > 0 और j > 2 के लिए, PA(i + 1, j) बहुपद_पदानुक्रम|Σ है<sub>i</sub><sup>PA</sup>-पूर्ण हैं। इस प्रकार अंतिम क्वांटिफायर ब्लॉक में कठोरता परिणाम के लिए केवल j>2 (j=1 के विपरीत) की आवश्यकता होती है।<br/>i>0 के लिए, PA(i+1) घातीय_पदानुक्रम या Σ<sub>i</sub><sup>EXP</sup>-पूर्ण (और समय परिवर्तन(2) है<sup>n<sup>O(i)</sup></sup>, i)-पूर्ण) है।{{sfn|Haase|2014|pp=47:1-47:10}}

छोटा <math>\Sigma_n</math> प्रेस्बर्गर अंकगणित (<math>n>2</math>) है <math>\Sigma_{n-2}^P</math> पूर्ण (और इस प्रकार एनपी पूर्ण के लिए <math>n=3</math>) हैं। यहां पर 'शॉर्ट' के लिए बाउंडेड (यानी) की आवश्यकता होती है। <math>O(1)</math>) वाक्य का आकार इसके अतिरिक्त इस पूर्णांक के लिए यह स्थिरांक असीमित हैं, अपितु बाइनरी में उनकी बिट्स की संख्या इनपुट आकार के विरुद्ध गिना जाता हैॉ। इसके आधार पर <math>\Sigma_2</math> दो परिवर्तनीय पीए 'संक्षिप्त' होने के प्रतिबंध के बिना एनपी-पूर्ण है।{{sfn|Nguyen|Pak|2017}} इसका मान कम से कम <math>\Pi_2</math> (और इस प्रकार <math>\Sigma_2</math>) PA में है, और यह निश्चित-आयामी पैरामीट्रिक पूर्णांक रैखिक प्रोग्रामिंग तक विस्तारित है।{{sfn|Eisenbrand|Shmonin|2008}}

==अनुप्रयोग==
क्योंकि प्रेस्बर्गर अंकगणित निर्णायक है, प्रेस्बर्गर अंकगणित के लिए स्वचालित प्रमेय सिद्धकर्ता उपस्थित हैं। उदाहरण के लिए, [[कॉक]] प्रूफ सहायक प्रणाली में प्रेस्बर्गर अंकगणित के लिए रणनीति ओमेगा की सुविधा है और इसाबेल (प्रूफ सहायक) में {{harvtxt|निपकोव|2010}} द्वारा सत्यापित क्वांटिफायर उन्मूलन प्रक्रिया सम्मिलित है। इसके सिद्धांत की दोहरी घातीय जटिलता जटिल सूत्रों पर प्रमेय कहावतों का उपयोग करना असंभव बनाती है, अपितु यह व्यवहार केवल नेस्टेड क्वांटिफायर की उपस्थिति में होता है: {{harvtxt|नेल्सेन|ओपेन्न|1978}} स्वचालित प्रमेय कहावत का वर्णन करें जो क्वांटिफायर-मुक्त प्रेस्बर्गर अंकगणित सूत्रों के कुछ उदाहरणों को प्रमाणित करने के लिए नेस्टेड क्वांटिफायर के बिना विस्तारित प्रेस्बर्गर अंकगणित पर [[सिम्प्लेक्स एल्गोरिथ्म|सिम्प्लेक्स कलन विधि]] का उपयोग करता है। वर्तमान समय में [[संतुष्टि मॉड्यूलो सिद्धांत]] सॉल्वर प्रेस्बर्गर अंकगणित सिद्धांत के क्वांटिफायर-मुक्त भाग को संभालने के लिए पूर्ण [[पूर्णांक प्रोग्रामिंग]] तकनीकों का उपयोग करते हैं।{{sfn|King|Barrett|Tinelli|2014}}

प्रेस्बर्गर अंकगणित को स्थिरांक द्वारा गुणन को सम्मिलित करने के लिए बढ़ाया जा सकता है, क्योंकि गुणन बार-बार जोड़ा जाता है। अधिकांश सरणी सबस्क्रिप्ट गणनाएँ निर्णय योग्य समस्याओं के क्षेत्र में आती हैं।<ref>For example, in the [[C (programming language)|C programming language]], if <code>a</code> is an array of 4 bytes element size, the expression <code>a[i]</code> can be translated to <code>a<sub>baseadr</sub>+i+i+i+i</code> which fits the restrictions of Presburger arithmetic.</ref> यह दृष्टिकोण [[कंप्यूटर प्रोग्राम|कंप्यूटर प्रोग्रामों]] के लिए कम से कम पांच प्रूफ-ऑफ-करेक्टनेस (कंप्यूटर विज्ञान) प्रणालियों का आधार है, जो 1970 के दशक के अंत में [[ स्टैनफोर्ड पास्कल सत्यापनकर्ता |स्टैनफोर्ड पास्कल सत्यापनकर्ता]] से शुरू हुआ और 2005 के माइक्रोसॉफ्ट के स्पेक सिस्टम तक प्रस्तुत किया हैं।

==प्रेस्बर्गर-निश्चित पूर्णांक संबंध==
अब '''प्रेस्बर्गर अंकगणित''' में परिभाषित पूर्णांक [[वित्तीय संबंध]] के बारे में कुछ गुण दिए गए हैं। सरलता के लिए, इस खंड में विचार किए गए सभी संबंध गैर-ऋणात्मक पूर्णांकों पर हैं।

एक संबंध प्रेस्बर्गर-परिभाषित है यदि और केवल यदि यह [[अर्धरेखीय सेट|अर्धरेखीय समुच्चय]] है।{{sfn|Ginsburg|Spanier|1966|pp=285–296}}

एक एकात्मक पूर्णांक से संबंधित <math>R</math>, अर्थात, गैर-ऋणात्मक पूर्णांकों का समुच्चय, प्रेस्बर्गर-परिभाषित है, इस प्रकार यदि यह अंततः आवधिक है। अर्थात्, यदि कोई सीमा <math>t\in \N</math> उपस्थित है और धनात्मक अवधि <math>p\in\N^{>0}</math> ऐसा कि, सभी पूर्णांकों के लिए <math>n</math> ऐसा है कि <math>|n|\ge t</math>, <math>n\in R</math> यदि <math>n+p\in R</math> पर निर्भर रहता हैं।

'''कोबम-सेमेनोव प्रमेय''' के अनुसार, संबंध प्रेस्बर्गर-परिभाषित है, कि यदि यह आधार के बुची अंकगणित में निश्चित है <math>k</math> सभी के लिए <math>k\ge2</math> हैं।{{sfn|Cobham|1969|pp=186–192}}{{sfn|Semenov|1977|pp=403–418}} इस प्रकार इसके आधार के बुची अंकगणित में परिभाषित संबंध <math>k</math> और <math>k'</math> के लिए <math>k</math> और <math>k'</math> गुणक स्वतंत्रता पूर्णांक होना प्रेस्बर्गर निश्चित है।

एक पूर्णांक संबंध <math>R</math> में प्रेस्बर्गर द्वारा परिभाषित है कि यदि जब पूर्णांकों के सभी समुच्चय जो पहले क्रम के तर्क में जोड़ और के साथ परिभाषित किए जा सकते हैं, जहाँ पर <math>R</math> (अर्थात, प्रेस्बर्गर अंकगणित प्लस के लिए विधेय <math>R</math>) प्रेस्बर्गर-परिभाषित हैं।{{sfn|Michaux|Villemaire|1996|pp=251–277}} इस प्रकार समान्य रूप से, प्रत्येक संबंध के लिए <math>R</math> जो कि प्रेस्बर्गर-परिभाषित नहीं है, इसमें अतिरिक्त और के साथ प्रथम-क्रम सूत्र उपस्थित है <math>R</math> जो पूर्णांकों के समुच्चय को परिभाषित करता है जिसे केवल जोड़ का उपयोग करके परिभाषित नहीं किया जा सकता है।

===मुचनिक की प्रमेय===
प्रेस्बर्गर-परिभाषित संबंध और लक्षण वर्णन स्वीकार करते हैं: मुचनिक की प्रमेय द्वारा{{sfn|Muchnik|2003|pp=1433–1444}} इसको स्पष्ट करना अधिक जटिल है, अपितु इससे दो पूर्व लक्षणों का प्रमाण मिल गये हैं। इस प्रकार मुचनिक के प्रमेय को बताने से पहले, कुछ अतिरिक्त परिभाषाएँ प्रस्तुत की जानी चाहिए।

होने देना <math>R\subseteq\N^d</math> समुच्चय हो, खंड <math>x_i = j</math> का <math>R</math>, के लिए <math>i < d</math> और <math>j \in \N</math> परिभाषित किया जाता है।
:<math>\left \{(x_0,\ldots,x_{i-1},x_{i+1},\ldots,x_{d-1})\in\N^{d-1}\mid(x_0,\ldots,x_{i-1},j,x_{i+1},\ldots,x_{d-1})\in R \right \}.</math>
इस प्रकार यहाँ पर दो समुच्चय <math>R,S\subseteq\N^d</math> और A {{nowrap|<math>d</math>-tuple}} दिए गए हैं। इसके लिए इन पूर्णांकों का <math>(p_0,\ldots,p_{d-1})\in\N^d</math>, समुच्चय <math>R</math> कहा जाता है, जिसके आधार पर <math>(p_0,\dots,p_{d-1})</math>-आवधिक में <math>S</math> यदि, सभी के लिए <math>(x_0, \dots, x_{d-1}) \in S</math> ऐसा है कि <math>(x_0+p_0,\dots,x_{d-1}+p_{d-1})\in S,</math> तब <math>(x_0,\ldots,x_{d-1})\in R</math> को इस प्रकार प्रदर्शित करते हैं यदि <math>(x_0+p_0,\dots,x_{d-1}+p_{d-1})\in R</math>. के लिए <math>s\in\N</math>, समुच्चय <math>R</math> बताया गया {{nowrap|<math>s</math>-periodic}} में <math>S</math> यदि इस प्रकार है कि {{nowrap|<math>(p_0,\ldots,p_{d-1})</math>-periodic}} होने पर इसके कुछ मान <math>(p_0,\dots,p_{d-1})\in\Z^d</math> होने पर उपयुक्त मान प्राप्त होता हैं-

:<math>\sum_{i=0}^{d-1}|p_i| < s.</math>
अंत में, के लिए <math>k,x_0,\dots,x_{d-1}\in\N</math> मान प्राप्त होता हैं।
:<math>C(k,(x_0,\ldots,x_{d-1}))= \left \{(x_0+c_0,\dots,x_{d-1}+c_{d-1})\mid 0 \leq c_i < k \right \}</math> आकार के घन <math>k</math> को निरूपित करते हैं, जिसका निचला कोना <math>(x_0,\dots,x_{d-1})</math> है।

{{math theorem|name=Muchnik's Theorem|math_statement= <math>R\subseteq\N^d</math> प्रेस्बर्गर-परिभाषित है यदि और केवल यदि:
* if <math>d > 1</math> फिर सभी अनुभाग <math>R</math> प्रेस्बर्गर-परिभाषित हैं और
* वहां सम्मिलित होने वाले <math>s\in\N</math> ऐसा कि, हर किसी के लिए <math>k\in\N</math>, जहाँ उपस्थित हैं <math>t\in\N</math> जिसका मान सभी के लिए इस प्रकार हैं कि <math>(x_0,\dots,x_{d-1})\in\N^d</math> जिसके साथ <math display="block">\sum_{i=0}^{d-1}x_i>t,</math> <math>R</math> हैं {{nowrap|<math>s</math>-periodic}} जिसमें <math>C(k,(x_0,\dots,x_{d-1}))</math>.}}

सहज रूप से, पूर्णांक <math>s</math> पारी की लंबाई, पूर्णांक का प्रतिनिधित्व करता है, यहाँ पर <math>k</math> घनों का आकार है और <math>t</math> आवधिकता से पहले की सीमा है। यह परिणाम तब सत्य रहता है, इस स्थिति के अनुसार-

:<math>\sum_{i=0}^{d-1}x_i>t</math> या तो द्वारा प्रतिस्थापित किया जाता है। 
:<math>\min(x_0,\ldots,x_{d-1})>t</math> या द्वारा <math>\max(x_0,\ldots,x_{d-1})>t</math> मान प्राप्त होता हैं।

इस लक्षण वर्णन ने प्रेस्बर्गर अंकगणित में निश्चितता के लिए तथाकथित निश्चित मानदंड को जन्म दिया हैं, अर्थात जोड़ और A के साथ प्रथम-क्रम सूत्र उपस्थित है, जिसके आधार पर {{nowrap|<math>d</math>-ary}} विधेय <math>R</math> जो यदि और केवल यदि को धारण करता है, इसके आधार पर <math>R</math> प्रेस्बर्गर-परिभाषित संबंध द्वारा व्याख्या की गई है। इस प्रकार मुचनिक का प्रमेय यह प्रमाणित करने की भी अनुमति देता है कि यह निर्णय लेने योग्य है कि [[स्वचालित अनुक्रम]] प्रेस्बर्गर-परिभाषित समुच्चय को स्वीकार करता है या नहीं यह स्वीकार किया जाता हैं।

==यह भी देखें==
*[[रॉबिन्सन अंकगणित]]
*[[स्कोलेम अंकगणित]]

==संदर्भ==
{{Reflist}}


==ग्रन्थसूची==
{{Refbegin}}

*{{cite journal
 |last= Berman
 |first= L.
 |year= 1980
 |title= The Complexity of Logical Theories
 |journal= Theoretical Computer Science
 |volume= 11
 |issue= 1
 |pages= 71–77
 |doi= 10.1016/0304-3975(80)90037-7
 |doi-access= free
}}

*{{cite journal
 |last= Cobham
 |first= Alan
 |author-link= Alan Cobham (mathematician)
 |year= 1969
 |title= On the base-dependence of sets of numbers recognizable by finite automata
 |journal= Math. Systems Theory
 |volume= 3
 |issue= 2
 |pages= 186–192
 |doi=10.1007/BF01746527
 |s2cid=19792434
}}

*{{Cite book
 |last= Cooper
 |first= D.C.
 |year= 1972
 |contribution= Theorem Proving in Arithmetic without Multiplication
 |title= Machine Intelligence
 |volume= 7
 |editor= B. Meltzer and D. Michie
 |publisher= Edinburgh University Press
 |pages= 91–99
}}

*{{cite journal
 |last1= Eisenbrand
 |first1= Friedrich
 |last2= Shmonin
 |first2= Gennady
 |year= 2008
 |title= Parametric Integer Programming in Fixed Dimension
 |journal= Mathematics of Operations Research
 |volume= 33
 |issue= 4
 |arxiv= 0801.4336
 |doi= 10.1287/moor.1080.0320 
}}

*{{Cite book
 |last= Enderton
 |first= Herbert
 |year= 2001
 |title= A mathematical introduction to logic
 |publisher= [[Academic Press]]
 |location= Boston, MA
 |edition= 2nd
 |isbn= 978-0-12-238452-3
}}

*{{cite book
 |last1= Ferrante
 |first1= Jeanne
 |author-link1= Jeanne Ferrante
 |last2= Rackoff
 |first2= Charles W.
 |year= 1979
 |title= The Computational Complexity of Logical Theories
 |series= Lecture Notes in Mathematics
 |volume= 718
 |publisher= [[Springer-Verlag]]
 |doi= 10.1007/BFb0062837
 |isbn= 978-3-540-09501-9
 |mr= 0537764
}}

*{{cite journal
 |last1= Fischer
 |first1= Michael J.
 |author-link1= Michael J. Fischer
 |last2= Rabin
 |first2= Michael O.
 |author-link2= Michael O. Rabin
 |year= 1974
 |title= Super-Exponential Complexity of Presburger Arithmetic
 |url= http://www.lcs.mit.edu/publications/pubs/ps/MIT-LCS-TM-043.ps
 |journal= Proceedings of the SIAM-AMS Symposium in Applied Mathematics
 |volume= 7
 |pages= 27–41
 |access-date= 2006-06-11
 |archive-url= https://web.archive.org/web/20060915010325/http://www.lcs.mit.edu/publications/pubs/ps/MIT-LCS-TM-043.ps
 |archive-date= 2006-09-15
 |url-status= dead
}}

*{{cite journal
 |last1= Ginsburg
 |first1= Seymour
 |author-link1= Seymour Ginsburg
 |last2= Spanier
 |first2= Edwin Henry
 |author-link2= Edwin Spanier
 |year= 1966
 |title= Semigroups, Presburger Formulas, and Languages
 |journal= Pacific Journal of Mathematics
 |volume= 16
 |issue= 2
 |pages= 285–296
 |doi=10.2140/pjm.1966.16.285
 |doi-access=free
}}

*{{cite conference
 | last= Haase
 | first= Christoph
 | year= 2014
 | title= Subclasses of Presburger Arithmetic and the Weak EXP Hierarchy
 | book-title= Proceedings CSL-LICS
 | publisher= ACM
 | pages= 47:1–47:10
 | doi= 10.1145/2603088.2603092
 | arxiv= 1401.5266
}}

*{{Cite journal
 |last= Haase
 |first= Christoph
 |year= 2018
 |title= A survival guide to presburger arithmetic
 |journal= ACM SIGLOG News
 |url= http://www.cs.ox.ac.uk/people/christoph.haase/home/publication/haa-18/haa-18.pdf
 |volume= 5
 |issue= 3
 |pages= 67–82
 |doi= 10.1145/3242953.3242964
 |s2cid= 51847374
}}

*{{cite book
 |last1= King
 |first1= Tim
 |last2= Barrett
 |first2= Clark W.
 |last3= Tinelli
 |first3= Cesare
 |year= 2014
 |title= 2014 Formal Methods In Computer-aided Design (fmcad 2014)
 |chapter= Leveraging linear and mixed integer programming for SMT
 |volume= 2014
 |pages= 139–146
 |doi= 10.1109/FMCAD.2014.6987606
 |isbn= 978-0-9835-6784-4
 |s2cid= 5542629
}}

*{{cite journal
 |last1= Michaux
 |first1= Christian
 |last2= Villemaire
 |first2= Roger
 |title= Presburger Arithmetic and Recognizability of Sets of Natural Numbers by Automata: New Proofs of Cobham's and Semenov's Theorems
 |journal= Ann. Pure Appl. Logic
 |date= 1996
 |volume= 77
 |issue= 3
 |pages= 251–277
 |doi= 10.1016/0168-0072(95)00022-4
 |doi-access= free
}}

*{{Cite book
 |last= Monk
 |first= J. Donald Monk
 |year= 2012
 |title= Mathematical Logic (Graduate Texts in Mathematics (37))
 |publisher= Springer
 |edition= Softcover reprint of the original 1st ed. 1976
 |isbn= 9781468494549
}}

*{{cite journal
 |last= Muchnik
 |first= Andrei A.
 |title= The definable criterion for definability in Presburger arithmetic and its applications
 |journal= Theor. Comput. Sci.
 |date= 2003
 |volume= 290
 |issue= 3
 |pages= 1433–1444
 |doi= 10.1016/S0304-3975(02)00047-6
 |doi-access= free
}}

*{{cite journal
 |last1= Nelson
 |first1= Greg
 |last2= Oppen
 |first2= Derek C.
 |date= April 1978
 |title= A simplifier based on efficient decision algorithms
 |journal= Proc. 5th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages
 |pages= 141–150
 |doi= 10.1145/512760.512775
 |s2cid= 6342372
}}

*{{cite journal
 |last1= Nguyen |first1= Danny
 |last2= Pak |first2= Igor |authorlink2=Igor Pak
 |year= 2017
 |title= Short Presburger Arithmetic Is Hard
 |journal= 2017 IEEE 58th Annual Symposium on Foundations of Computer Science (FOCS)
 |url= http://www.math.ucla.edu/~pak/papers/hard_presburger3.pdf
 |access-date= 2022-09-04
 |arxiv= 1708.08179
 |doi= 10.1109/FOCS.2017.13 
}}

*{{cite thesis
 |last= Nguyen Luu
 |first= Dahn
 |year= 2018
 |title= The Computational Complexity of Presburger Arithmetic
 |publisher= UCLA Electronic Theses and Dissertations
 |location= Los Angeles
 |url= https://escholarship.org/uc/item/6j9051vs
 |access-date= 2022-09-08
}}

*{{cite journal
 |last= Nipkow
 |first= T
 |year= 2010
 |title= Linear Quantifier Elimination
 |url= http://www4.cs.tum.edu/~nipkow/pubs/ijcar08.pdf
 |journal= Journal of Automated Reasoning
 |volume= 45
 |issue= 2
 |pages= 189–212
 |doi= 10.1007/s10817-010-9183-0
 |s2cid= 14279141
}}

*{{cite journal
 |last= Oppen
 |first= Derek C.
 |year= 1978
 |title= A 2<sup>2<sup>2<sup>''pn''</sup></sup></sup> Upper Bound on the Complexity of Presburger Arithmetic
 |journal= J. Comput. Syst. Sci.
 |volume= 16
 |issue= 3
 |pages= 323–332
 |doi= 10.1016/0022-0000(78)90021-1
 |doi-access= free
}}

*{{cite journal
 |last= Presburger
 |first= Mojżesz
 |author-link= Mojżesz Presburger
 |date= 1929
 |title= Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt
 |journal= Comptes Rendus du I congrès de Mathématiciens des Pays Slaves, Warszawa
 |pages= 92–101
}}, see {{harvtxt|Stansifer|1984}} for an English translation

*{{cite journal
 |last= Pugh
 |first= William
 |author-link= William Pugh (computer scientist)
 |year= 1991
 |title= The Omega test: a fast and practical integer programming algorithm for dependence analysis
 |journal= Supercomputing '91: Proceedings of the 1991 ACM/IEEE Conference on Supercomputing
 |pages= 4–13
 |publisher = Association for Computing Machinery
 |publication-place= New York, NY, USA
 |doi= 10.1145/125826.125848
 |isbn= 0897914597
 |s2cid= 3174094
 }}

*{{cite journal
 |last1= Reddy
 |first1= C.R.
 |last2= Loveland
 |first2= D.W.
 |year= 1978
 |title= Presburger Arithmetic with Bounded Quantifier Alternation
 |journal= ACM Symposium on Theory of Computing
 |pages = 320–325
 |doi= 10.1145/800133.804361
 |s2cid= 13966721
}}

*{{cite journal
 |first= A.L.
 |last= Semenov
 |year= 1977
 |title= Presburgerness of predicates regular in two number systems
 |language= ru
 |journal= Sibirsk. Mat. Zh.
 |volume= 18
 |pages= 403–418
}}

*{{cite report
 |last= Stansifer
 |first= Ryan
 |date= Sep 1984
 |title= Presburger's Article on Integer Arithmetic: Remarks and Translation
 |type= Technical Report
 |location= Ithaca/NY
 |publisher= Dept. of Computer Science, Cornell University
 |volume= TR84-639
 |url= http://cs.fit.edu/~ryan/papers/presburger.pdf
}}

*{{cite book
 |last= Young
 |first= P.
 |year= 1985
 |contribution= Gödel theorems, exponential difficulty and undecidability of arithmetic theories: an exposition
 |title= Recursion Theory, American Mathematical Society
 |editor= A. Nerode and R. Shore
 |pages= 503–522
}}

*{{cite thesis
 |last= Zoethout
 |first= Jetze
 |date= February 1, 2015
 |title= Interpretations in Presburger Arithmetic (Bachelor Thesis)
 |url= https://dspace.library.uu.nl/bitstream/handle/1874/315291/Thesis.pdf
 |access-date= 2021-10-25
 }}

{{Refend}}


==बाहरी संबंध==
*[http://www.philipp.ruemmer.org/princess.shtml A complete Theorem Prover for Presburger Arithmetic] by Philipp Rümmer

[[Category:1929 परिचय]]
[[Category:CS1]]
[[Category:CS1 русский-language sources (ru)]]
[[Category:Created On 27/06/2023]]
[[Category:Lua-based templates]]
[[Category:Machine Translated Page]]
[[Category:Pages with script errors]]
[[Category:Templates Vigyan Ready]]
[[Category:Templates that add a tracking category]]
[[Category:Templates that generate short descriptions]]
[[Category:Templates using TemplateData]]
[[Category:अंकगणित के औपचारिक सिद्धांत]]
[[Category:कंप्यूटर विज्ञान में तर्क]]
[[Category:प्रमाण सिद्धांत]]
[[Category:मॉडल सिद्धांत]]