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

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

प्रेस्बर्गर अंकगणित पीनो अंकगणित की तुलना में बहुत कमजोर है, जिसमें जोड़ और गुणा दोनों ऑपरेशन शामिल हैं। पीनो अंकगणित के विपरीत, प्रेस्बर्गर अंकगणित एक निर्णायकता (तर्क) है। इसका मतलब यह है कि प्रेस्बर्गर अंकगणित की भाषा में किसी भी वाक्य के लिए एल्गोरिदमिक रूप से यह निर्धारित करना संभव है कि क्या वह वाक्य प्रेस्बर्गर अंकगणित के सिद्धांतों से साबित करने योग्य है। हालाँकि, इस एल्गोरिथ्म के एल्गोरिदम का एसिम्प्टोटिक रनिंग-टाइम विश्लेषण कम से कम दोहरा घातीय कार्य है, जैसा कि दिखाया गया है Fischer & Rabin (1974).

अवलोकन

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

इस भाषा में, प्रेस्बर्गर अंकगणित के स्वयंसिद्ध निम्नलिखित के सार्वभौमिक समापन हैं:

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

(5) गणितीय प्रेरण की एक स्वयंसिद्ध स्कीमा है, जो अनंत रूप से कई स्वयंसिद्धों का प्रतिनिधित्व करती है। इन्हें किसी भी सीमित संख्या में स्वयंसिद्धों द्वारा प्रतिस्थापित नहीं किया जा सकता है, अर्थात, प्रेस्बर्गर अंकगणित प्रथम-क्रम तर्क में अंतिम रूप से स्वयंसिद्ध नहीं है।

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

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

गुण

मोजेज़ प्रेस्बर्गर ने प्रेस्बर्गर अंकगणित को सिद्ध किया:

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

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

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

कम्प्यूटेशनल जटिलता

प्रेस्बर्गर अंकगणित के लिए निर्णय समस्या कम्प्यूटेशनल जटिलता सिद्धांत और गणना में एक दिलचस्प उदाहरण है। मान लीजिए कि प्रेस्बर्गर अंकगणित में एक कथन की लंबाई n है। तब Fischer & Rabin (1974) साबित हुआ कि, सबसे खराब स्थिति में, पहले क्रम के तर्क में कथन के प्रमाण की लंबाई कम से कम होती है $2^{2^{cn}}$, कुछ स्थिरांक c>0 के लिए। इसलिए, प्रेस्बर्गर अंकगणित के लिए उनके निर्णय एल्गोरिदम का रनटाइम कम से कम घातीय है। फिशर और राबिन ने यह भी साबित किया कि किसी भी उचित स्वयंसिद्धीकरण (उनके पेपर में सटीक रूप से परिभाषित) के लिए, लंबाई n के प्रमेय मौजूद हैं जिनमें दोहरे घातीय फ़ंक्शन लंबाई प्रमाण हैं। सहज रूप से, इससे पता चलता है कि कंप्यूटर प्रोग्राम द्वारा क्या सिद्ध किया जा सकता है, इसकी कम्प्यूटेशनल सीमाएँ हैं। फिशर और राबिन के काम का यह भी तात्पर्य है कि प्रेस्बर्गर अंकगणित का उपयोग उन सूत्रों को परिभाषित करने के लिए किया जा सकता है जो किसी भी एल्गोरिदम की सही गणना करते हैं जब तक कि इनपुट अपेक्षाकृत बड़ी सीमा से कम न हो। सीमाएँ बढ़ाई जा सकती हैं, लेकिन केवल नए फ़ार्मुलों का उपयोग करके। दूसरी ओर, प्रेस्बर्गर अंकगणित के लिए निर्णय प्रक्रिया पर एक त्रिगुण घातीय ऊपरी सीमा किसके द्वारा सिद्ध की गई थी? Oppen (1978).

वैकल्पिक जटिलता वर्गों का उपयोग करके एक अधिक सख्त जटिलता सीमा दिखाई गई थी Berman (1980). प्रेस्बर्गर अंकगणित (पीए) में सत्य कथनों का सेट वैकल्पिक ट्यूरिंग मशीन (2) के लिए पूरा दिखाया गया है^2nO(1), n). इस प्रकार, इसकी जटिलता दोहरे घातीय गैर-नियतात्मक समय (2-NEXP) और दोहरे घातीय स्थान (2-EXPSPACE) के बीच है। पूर्णता बहुपद समय अनेक-से-एक कटौती के अंतर्गत है। (यह भी ध्यान दें कि प्रेस्बर्गर अंकगणित को आमतौर पर पीए के रूप में संक्षिप्त किया जाता है, गणित में सामान्य तौर पर पीए का मतलब आमतौर पर पीनो अंकगणित होता है।)

अधिक सुक्ष्म परिणाम के लिए, मान लें कि PA(i) सत्य Σ का समुच्चय है_i PA कथन, और PA(i, j) सत्य Σ का समुच्चय_i प्रत्येक क्वांटिफायर ब्लॉक के साथ पीए स्टेटमेंट जे वेरिएबल्स तक सीमित हैं। '<' को क्वांटिफायर-मुक्त माना जाता है; यहां, परिबद्ध परिमाणकों को परिमाणकों के रूप में गिना जाता है।
PA(1, j) P में है, जबकि PA(1) NP-पूर्ण है।
i > 0 और j > 2 के लिए, PA(i + 1, j) बहुपद_पदानुक्रम|Σ है_i^प-पूर्ण। अंतिम क्वांटिफायर ब्लॉक में कठोरता परिणाम के लिए केवल j>2 (j=1 के विपरीत) की आवश्यकता होती है।
i>0 के लिए, PA(i+1) घातीय_पदानुक्रम|Σ है_i^EXP-पूर्ण (और समय परिवर्तन(2) है^nO(i), i)-पूर्ण).

छोटा $\Sigma _{n}$ प्रेस्बर्गर अंकगणित ($n>2$) है $\Sigma _{n-2}^{P}$ पूर्ण (और इस प्रकार एनपी पूर्ण के लिए $n=3$). यहां, 'शॉर्ट' के लिए बाउंडेड (यानी) की आवश्यकता होती है। $O(1)$) वाक्य का आकार, सिवाय इसके कि पूर्णांक स्थिरांक असीमित हैं (लेकिन बाइनरी में उनकी बिट्स की संख्या इनपुट आकार के विरुद्ध गिना जाता है)। भी, $\Sigma _{2}$ दो परिवर्तनीय पीए ('संक्षिप्त' होने के प्रतिबंध के बिना) एनपी-पूर्ण है। छोटा $\Pi _{2}$ (और इस तरह $\Sigma _{2}$) पीए पी में है, और यह निश्चित-आयामी पैरामीट्रिक पूर्णांक रैखिक प्रोग्रामिंग तक विस्तारित है।

अनुप्रयोग

क्योंकि प्रेस्बर्गर अंकगणित निर्णायक है, प्रेस्बर्गर अंकगणित के लिए स्वचालित प्रमेय सिद्धकर्ता मौजूद हैं। उदाहरण के लिए, कॉक प्रूफ सहायक प्रणाली में प्रेस्बर्गर अंकगणित के लिए रणनीति ओमेगा की सुविधा है और इसाबेल (प्रूफ सहायक) में एक सत्यापित क्वांटिफायर उन्मूलन प्रक्रिया शामिल है Nipkow (2010). सिद्धांत की दोहरी घातीय जटिलता जटिल सूत्रों पर प्रमेय कहावतों का उपयोग करना असंभव बनाती है, लेकिन यह व्यवहार केवल नेस्टेड क्वांटिफायर की उपस्थिति में होता है: Nelson & Oppen (1978) एक स्वचालित प्रमेय कहावत का वर्णन करें जो क्वांटिफायर-मुक्त प्रेस्बर्गर अंकगणित सूत्रों के कुछ उदाहरणों को साबित करने के लिए नेस्टेड क्वांटिफायर के बिना विस्तारित प्रेस्बर्गर अंकगणित पर सिम्प्लेक्स एल्गोरिथ्म का उपयोग करता है। हालिया संतुष्टि मॉड्यूलो सिद्धांत सॉल्वर प्रेस्बर्गर अंकगणित सिद्धांत के क्वांटिफायर-मुक्त टुकड़े को संभालने के लिए पूर्ण पूर्णांक प्रोग्रामिंग तकनीकों का उपयोग करते हैं।

प्रेस्बर्गर अंकगणित को स्थिरांक द्वारा गुणन को शामिल करने के लिए बढ़ाया जा सकता है, क्योंकि गुणन बार-बार जोड़ा जाता है। अधिकांश सरणी सबस्क्रिप्ट गणनाएँ निर्णय योग्य समस्याओं के क्षेत्र में आती हैं। यह दृष्टिकोण कंप्यूटर प्रोग्रामों के लिए कम से कम पांच प्रूफ-ऑफ-करेक्टनेस (कंप्यूटर विज्ञान) प्रणालियों का आधार है, जो 1970 के दशक के अंत में स्टैनफोर्ड पास्कल सत्यापनकर्ता से शुरू हुआ और 2005 के माइक्रोसॉफ्ट के स्पेक # सिस्टम तक जारी रहा।

प्रेस्बर्गर-निश्चित पूर्णांक संबंध

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

एक संबंध प्रेस्बर्गर-परिभाषित है यदि और केवल यदि यह एक अर्धरेखीय सेट है।

एक एकात्मक पूर्णांक संबंध $R$, अर्थात, गैर-नकारात्मक पूर्णांकों का एक सेट, प्रेस्बर्गर-परिभाषित है यदि और केवल यदि यह अंततः आवधिक है। अर्थात्, यदि कोई सीमा मौजूद है $t\in \mathbb {N}$ और एक सकारात्मक अवधि $p\in \mathbb {N} ^{>0}$ ऐसा कि, सभी पूर्णांकों के लिए $n$ ऐसा है कि $|n|\geq t$, $n\in R$ अगर और केवल अगर $n+p\in R$.

कोबम-सेमेनोव प्रमेय के अनुसार, एक संबंध प्रेस्बर्गर-परिभाषित है यदि और केवल यदि यह आधार के बुची अंकगणित में निश्चित है $k$ सभी के लिए $k\geq 2$. आधार के बुची अंकगणित में परिभाषित एक संबंध $k$ और $k'$ के लिए $k$ और $k'$ गुणक स्वतंत्रता पूर्णांक होना प्रेस्बर्गर निश्चित है।

एक पूर्णांक संबंध $R$ प्रेस्बर्गर-परिभाषित है यदि और केवल तभी जब पूर्णांकों के सभी सेट जो पहले क्रम के तर्क में जोड़ और के साथ परिभाषित किए जा सकते हैं $R$ (अर्थात, प्रेस्बर्गर अंकगणित प्लस के लिए एक विधेय $R$) प्रेस्बर्गर-परिभाषित हैं। समान रूप से, प्रत्येक संबंध के लिए $R$ जो कि प्रेस्बर्गर-परिभाषित नहीं है, इसमें अतिरिक्त और के साथ एक प्रथम-क्रम सूत्र मौजूद है $R$ जो पूर्णांकों के एक सेट को परिभाषित करता है जिसे केवल जोड़ का उपयोग करके परिभाषित नहीं किया जा सकता है।

मुचनिक का चरित्र-चित्रण

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

होने देना $R\subseteq \mathbb {N} ^{d}$ एक समुच्चय हो, खंड $x_{i}=j$ का $R$, के लिए $i<d$ और $j\in \mathbb {N}$ परिभाषित किया जाता है

$\left\{(x_{0},\ldots ,x_{i-1},x_{i+1},\ldots ,x_{d-1})\in \mathbb {N} ^{d-1}\mid (x_{0},\ldots ,x_{i-1},j,x_{i+1},\ldots ,x_{d-1})\in R\right\}.$

दो सेट दिए गए $R,S\subseteq \mathbb {N} ^{d}$ और ए $d$-tuple पूर्णांकों का $(p_{0},\ldots ,p_{d-1})\in \mathbb {N} ^{d}$, सेट $R$ कहा जाता है $(p_{0},\dots ,p_{d-1})$-आवधिक में $S$ यदि, सभी के लिए $(x_{0},\dots ,x_{d-1})\in S$ ऐसा है कि $(x_{0}+p_{0},\dots ,x_{d-1}+p_{d-1})\in S,$ तब $(x_{0},\ldots ,x_{d-1})\in R$ अगर और केवल अगर $(x_{0}+p_{0},\dots ,x_{d-1}+p_{d-1})\in R$. के लिए $s\in \mathbb {N}$, सेट $R$ बताया गया $s$-periodic में $S$ अगर यह है $(p_{0},\ldots ,p_{d-1})$-periodic कुछ के लिए $(p_{0},\dots ,p_{d-1})\in \mathbb {Z} ^{d}$ ऐसा है कि

$\sum _{i=0}^{d-1}|p_{i}|<s.$

अंत में, के लिए $k,x_{0},\dots ,x_{d-1}\in \mathbb {N}$ होने देना

$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\}$ आकार के घन को निरूपित करें $k$ जिसका निचला कोना है $(x_{0},\dots ,x_{d-1})$.

Muchnik's Theorem — $R\subseteq \mathbb {N} ^{d}$ is Presburger-definable if and only if:

• if $d>1$ then all sections of $R$ are Presburger-definable and
• there exists $s\in \mathbb {N}$ such that, for every $k\in \mathbb {N}$, there exists $t\in \mathbb {N}$ such that for all $(x_{0},\dots ,x_{d-1})\in \mathbb {N} ^{d}$ with
  $$\sum _{i=0}^{d-1}x_{i}>t,$$
  $R$ is $s$-periodic in $C(k,(x_{0},\dots ,x_{d-1}))$.

सहज रूप से, पूर्णांक $s$ एक पारी की लंबाई, पूर्णांक का प्रतिनिधित्व करता है $k$ घनों का आकार है और $t$ आवधिकता से पहले की सीमा है। यह परिणाम तब सत्य रहता है जब स्थिति

$\sum _{i=0}^{d-1}x_{i}>t$ या तो द्वारा प्रतिस्थापित किया जाता है $\min(x_{0},\ldots ,x_{d-1})>t$ या द्वारा $\max(x_{0},\ldots ,x_{d-1})>t$.

इस लक्षण वर्णन ने प्रेस्बर्गर अंकगणित में निश्चितता के लिए तथाकथित निश्चित मानदंड को जन्म दिया, अर्थात: जोड़ और ए के साथ प्रथम-क्रम सूत्र मौजूद है $d$-ary विधेय $R$ जो यदि और केवल यदि को धारण करता है $R$ प्रेस्बर्गर-परिभाषित संबंध द्वारा व्याख्या की गई है। मुचनिक का प्रमेय यह साबित करने की भी अनुमति देता है कि यह निर्णय लेने योग्य है कि स्वचालित अनुक्रम प्रेस्बर्गर-परिभाषित सेट को स्वीकार करता है या नहीं।

यह भी देखें

• रॉबिन्सन अंकगणित
• स्कोलेम अंकगणित

ग्रन्थसूची

• Berman, L. (1980). "The Complexity of Logical Theories". Theoretical Computer Science. 11 (1): 71–77. doi:10.1016/0304-3975(80)90037-7.

• Cobham, Alan (1969). "On the base-dependence of sets of numbers recognizable by finite automata". Math. Systems Theory. 3 (2): 186–192. doi:10.1007/BF01746527. S2CID 19792434.

• Cooper, D.C. (1972). "Theorem Proving in Arithmetic without Multiplication". In B. Meltzer and D. Michie (ed.). Machine Intelligence. Vol. 7. Edinburgh University Press. pp. 91–99.

• Eisenbrand, Friedrich; Shmonin, Gennady (2008). "Parametric Integer Programming in Fixed Dimension". Mathematics of Operations Research. 33 (4). arXiv:0801.4336. doi:10.1287/moor.1080.0320.

• Enderton, Herbert (2001). A mathematical introduction to logic (2nd ed.). Boston, MA: Academic Press. ISBN 978-0-12-238452-3.

• Ferrante, Jeanne; Rackoff, Charles W. (1979). The Computational Complexity of Logical Theories. Lecture Notes in Mathematics. Vol. 718. Springer-Verlag. doi:10.1007/BFb0062837. ISBN 978-3-540-09501-9. MR 0537764.

• Fischer, Michael J.; Rabin, Michael O. (1974). "Super-Exponential Complexity of Presburger Arithmetic". Proceedings of the SIAM-AMS Symposium in Applied Mathematics. 7: 27–41. Archived from the original on 2006-09-15. Retrieved 2006-06-11.

• Ginsburg, Seymour; Spanier, Edwin Henry (1966). "Semigroups, Presburger Formulas, and Languages". Pacific Journal of Mathematics. 16 (2): 285–296. doi:10.2140/pjm.1966.16.285.

• Haase, Christoph (2014). "Subclasses of Presburger Arithmetic and the Weak EXP Hierarchy". Proceedings CSL-LICS. ACM. pp. 47:1–47:10. arXiv:1401.5266. doi:10.1145/2603088.2603092.

• Haase, Christoph (2018). "A survival guide to presburger arithmetic" (PDF). ACM SIGLOG News. 5 (3): 67–82. doi:10.1145/3242953.3242964. S2CID 51847374.

• King, Tim; Barrett, Clark W.; Tinelli, Cesare (2014). "Leveraging linear and mixed integer programming for SMT". 2014 Formal Methods In Computer-aided Design (fmcad 2014). Vol. 2014. pp. 139–146. doi:10.1109/FMCAD.2014.6987606. ISBN 978-0-9835-6784-4. S2CID 5542629.

• Michaux, Christian; Villemaire, Roger (1996). "Presburger Arithmetic and Recognizability of Sets of Natural Numbers by Automata: New Proofs of Cobham's and Semenov's Theorems". Ann. Pure Appl. Logic. 77 (3): 251–277. doi:10.1016/0168-0072(95)00022-4.

• Monk, J. Donald Monk (2012). Mathematical Logic (Graduate Texts in Mathematics (37)) (Softcover reprint of the original 1st ed. 1976 ed.). Springer. ISBN 9781468494549.

• Muchnik, Andrei A. (2003). "The definable criterion for definability in Presburger arithmetic and its applications". Theor. Comput. Sci. 290 (3): 1433–1444. doi:10.1016/S0304-3975(02)00047-6.

• Nelson, Greg; Oppen, Derek C. (April 1978). "A simplifier based on efficient decision algorithms". Proc. 5th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages: 141–150. doi:10.1145/512760.512775. S2CID 6342372.

• Nguyen, Danny; Pak, Igor (2017). "Short Presburger Arithmetic Is Hard" (PDF). 2017 IEEE 58th Annual Symposium on Foundations of Computer Science (FOCS). arXiv:1708.08179. doi:10.1109/FOCS.2017.13. Retrieved 2022-09-04.

• Nguyen Luu, Dahn (2018). The Computational Complexity of Presburger Arithmetic (Thesis). Los Angeles: UCLA Electronic Theses and Dissertations. Retrieved 2022-09-08.

• Nipkow, T (2010). "Linear Quantifier Elimination" (PDF). Journal of Automated Reasoning. 45 (2): 189–212. doi:10.1007/s10817-010-9183-0. S2CID 14279141.

• Oppen, Derek C. (1978). "A 2^22pn Upper Bound on the Complexity of Presburger Arithmetic". J. Comput. Syst. Sci. 16 (3): 323–332. doi:10.1016/0022-0000(78)90021-1.

• Presburger, Mojżesz (1929). "Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt". Comptes Rendus du I congrès de Mathématiciens des Pays Slaves, Warszawa: 92–101., see Stansifer (1984) for an English translation

• Pugh, William (1991). "The Omega test: a fast and practical integer programming algorithm for dependence analysis". Supercomputing '91: Proceedings of the 1991 ACM/IEEE Conference on Supercomputing. New York, NY, USA: Association for Computing Machinery: 4–13. doi:10.1145/125826.125848. ISBN 0897914597. S2CID 3174094.

• Reddy, C.R.; Loveland, D.W. (1978). "Presburger Arithmetic with Bounded Quantifier Alternation". ACM Symposium on Theory of Computing: 320–325. doi:10.1145/800133.804361. S2CID 13966721.

• Semenov, A.L. (1977). "Presburgerness of predicates regular in two number systems". Sibirsk. Mat. Zh. (in русский). 18: 403–418.

• Stansifer, Ryan (Sep 1984). Presburger's Article on Integer Arithmetic: Remarks and Translation (PDF) (Technical Report). Vol. TR84-639. Ithaca/NY: Dept. of Computer Science, Cornell University.

• Young, P. (1985). "Gödel theorems, exponential difficulty and undecidability of arithmetic theories: an exposition". In A. Nerode and R. Shore (ed.). Recursion Theory, American Mathematical Society. pp. 503–522.

• Zoethout, Jetze (February 1, 2015). Interpretations in Presburger Arithmetic (Bachelor Thesis) (PDF) (Thesis). Retrieved 2021-10-25.

बाहरी संबंध

• A complete Theorem Prover for Presburger Arithmetic by Philipp Rümmer