1617:
407:
length proofs. Intuitively, this suggests there are computational limits on what can be proven by computer programs. Fischer and Rabin's work also implies that
Presburger arithmetic can be used to define formulas that correctly calculate any algorithm as long as the inputs are less than relatively
302:
that decides whether any given statement in
Presburger arithmetic is a theorem or a nontheorem - note that a "nontheorem" is a formula that cannot be proved, not in general necessarily one whose negation can be proved, but in the case of a complete theory like here both definitions are
1234:
Presburger-definable relations admit another characterization: by
Muchnik's theorem. It is more complicated to state, but led to the proof of the two former characterizations. Before Muchnik's theorem can be stated, some additional definitions must be introduced.
2735:
737:
Presburger arithmetic can be extended to include multiplication by constants, since multiplication is repeated addition. Most array subscript calculations then fall within the region of decidable problems. This approach is the basis of at least five
399:>0. Hence, their decision algorithm for Presburger arithmetic has runtime at least exponential. Fischer and Rabin also proved that for any reasonable axiomatization (defined precisely in their paper), there exist theorems of length
1386:
69:. This means it is possible to algorithmically determine, for any sentence in the language of Presburger arithmetic, whether that sentence is provable from the axioms of Presburger arithmetic. The asymptotic running-time
1757:
3070:
2403:
2018:
2178:
2548:
3513:
3446:
718:. The double exponential complexity of the theory makes it infeasible to use the theorem provers on complicated formulas, but this behavior occurs only in the presence of nested quantifiers:
408:
large bounds. The bounds can be increased, but only by using new formulas. On the other hand, a triply exponential upper bound on a decision procedure for
Presburger arithmetic was proved by
2479:
1661:
3133:
2556:
2082:
3376:
3248:
2860:
1919:
1271:
856:
2328:
2816:
1835:
214:, representing infinitely many axioms. These cannot be replaced by any finite number of axioms, that is, Presburger arithmetic is not finitely axiomatizable in first-order logic.
4324:
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".
236:, or, more generally, any number concept leading to multiplication of variables. However, it can formulate individual instances of divisibility; for example, it proves "for all
2997:
2969:
2941:
2206:
1378:
818:
556:
315:. The steps used to justify a quantifier elimination algorithm can be used to define computable axiomatizations that do not necessarily contain the axiom schema of induction.
3518:
This characterization led to the so-called "definable criterion for definability in
Presburger arithmetic", that is: there exists a first-order formula with addition and a
423:(2, n). Thus, its complexity is between double exponential nondeterministic time (2-NEXP) and double exponential space (2-EXPSPACE). Completeness is under polynomial time
692:
638:
492:
393:
912:
970:
665:
1304:
1117:
1072:
1027:
2890:
1350:
938:
518:
611:
442:
PA statements with each quantifier block limited to j variables. '<' is considered to be quantifier-free; here, bounded quantifiers are counted as quantifiers.
582:
3579:
3559:
3537:
3313:
3293:
3273:
3173:
3152:
2910:
2758:
2269:
2247:
2226:
1855:
1777:
1682:
1612:{\displaystyle \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\}.}
1324:
1224:
1204:
1184:
1164:
1144:
1092:
1047:
1001:
876:
790:
726:
on an extended
Presburger arithmetic without nested quantifiers to prove some of the instances of quantifier-free Presburger arithmetic formulas. More recent
221:
with equality containing precisely all consequences of the above axioms. Alternatively, it can be defined as the set of those sentences that are true in the
292:: For each statement in the language of Presburger arithmetic, either it is possible to deduce it from the axioms or it is possible to deduce its negation.
4707:
Young, P. (1985). "Gödel theorems, exponential difficulty and undecidability of arithmetic theories: an exposition". In A. Nerode and R. Shore (ed.).
4583:(1929). "Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt".
792:, that is, a set of non-negative integers, is Presburger-definable if and only if it is ultimately periodic. That is, if there exists a threshold
4767:
3866:
4464:
4304:
4120:
4076:
4040:
4104:
322:, which is Presburger arithmetic augmented with multiplication, is not decidable, as proved by Church alongside the negative answer to the
327:
762:
definable in
Presburger Arithmetic. For the sake of simplicity, all relations considered in this section are over non-negative integers.
4772:
3986:
4599:
4358:
613:) sentence size except that integer constants are unbounded (but their number of bits in binary counts against input size). Also,
3075:
4326:
1689:
3002:
2335:
1924:
286:: There is no statement in Presburger arithmetic that can be deduced from the axioms such that its negation can also be deduced.
2087:
343:
3581:
is interpreted by a
Presburger-definable relation. Muchnik's theorem also allows one to prove that it is decidable whether an
4629:
4519:
4267:
4164:
739:
727:
39:
23:
2487:
331:
4112:
4762:
3921:
3451:
3384:
1146:
is
Presburger-definable if and only if all sets of integers that are definable in first-order logic with addition and
1120:
427:. (Also, note that while Presburger arithmetic is commonly abbreviated PA, in mathematics in general PA usually means
404:
74:
2730:{\displaystyle 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\}}
976:
2411:
4222:
3971:
1625:
711:
420:
89:
The language of Presburger arithmetic contains constants 0 and 1 and a binary function +, interpreted as addition.
2023:
65:, which includes both addition and multiplication operations. Unlike Peano arithmetic, Presburger arithmetic is a
4287:
King, Tim; Barrett, Clark W.; Tinelli, Cesare (2014). "Leveraging linear and mixed integer programming for SMT".
4192:
3911:
3321:
3180:
2830:
1860:
1241:
228:
Presburger arithmetic is designed to be complete and decidable. Therefore, it cannot formalize concepts such as
3766:
823:
703:
747:
4719:
2275:
3891:
2763:
1782:
4607:
308:
222:
211:
70:
55:
43:
225:: the structure of non-negative integers with constants 0, 1, and the addition of non-negative integers.
4782:
4777:
4556:
4279:
In this paper a procedure for constructing an automaton that decides Presburger arithmetic is explained.
457:
424:
4580:
2974:
2946:
2918:
2183:
1355:
795:
523:
35:
4602:(1991). "The Omega test: A fast and practical integer programming algorithm for dependence analysis".
3981:
447:
323:
295:
289:
66:
358:
proved that, in the worst case, the proof of the statement in first-order logic has length at least
4612:
4399:
Nelson, Greg; Oppen, Derek C. (April 1978). "A simplifier based on efficient decision algorithms".
3956:
3594:
980:
731:
4700:(Technical Report). Vol. TR84-639. Ithaca/NY: Dept. of Computer Science, Cornell University.
4662:
4649:
Reddy, C.R.; Loveland, D.W. (1978). "Presburger arithmetic with bounded quantifier alternation".
4635:
4536:
4470:
4442:
4412:
4310:
4245:
4197:
4096:
4013:
3995:
3941:
3582:
670:
616:
470:
312:
4134:
361:
881:
4678:
4625:
4460:
4354:
4300:
4126:
4116:
4072:
4036:
3599:
943:
759:
743:
723:
643:
283:
218:
160:
93:
1276:
1006:
4654:
4617:
4564:
4528:
4452:
4431:
4404:
4383:
4335:
4292:
4237:
4207:
4173:
4151:
4100:
4064:
4005:
3933:
3875:
2869:
1329:
917:
497:
428:
319:
62:
4189:
Haase, Christoph (2014). "Subclasses of Presburger Arithmetic and the Weak EXP Hierarchy".
4086:
694:) PA is in P, and this extends to fixed-dimensional parametric integer linear programming.
4082:
4060:
4052:
587:
561:
454:. The hardness result only needs j>2 (as opposed to j=1) in the last quantifier block.
330:, Peano arithmetic is incomplete and its consistency is not internally provable (but see
4372:"The definable criterion for definability in Presburger arithmetic and its applications"
1097:
1052:
4032:
3899:
3564:
3544:
3522:
3298:
3278:
3258:
3158:
3137:
2895:
2743:
2254:
2232:
2211:
1840:
1762:
1667:
1309:
1209:
1206:
that is not Presburger-definable, there exists a first-order formula with addition and
1189:
1169:
1149:
1129:
1077:
1032:
986:
861:
775:
766:
707:
51:
47:
27:
4388:
4371:
3315:
is the threshold before the periodicity. This result remains true when the condition
4756:
4569:
4551:
4339:
4155:
3924:(1969). "On the base-dependence of sets of numbers recognizable by finite automata".
3903:
3880:
3861:
4676:
Semenov, A.L. (1977). "Presburgerness of predicates regular in two number systems".
4666:
4540:
4249:
4017:
3945:
4639:
4474:
4416:
4314:
3895:
710:
proof assistant system features the tactic omega for Presburger arithmetic and the
229:
207:
4604:
Proceedings of the 1991 ACM/IEEE conference on Supercomputing - Supercomputing '91
4511:
4260:
640:
two variable PA (without the restriction of being 'short') is NP-complete. Short
419:. The set of true statements in Presburger arithmetic (PA) is shown complete for
4746:
4694:
3984:; Shmonin, Gennady (2008). "Parametric Integer Programming in Fixed Dimension".
415:
A more tight complexity bound was shown using alternating complexity classes by
347:
4651:
Proceedings of the tenth annual ACM symposium on Theory of computing - STOC '78
4296:
734:
techniques to handle quantifier-free fragment of Presburger arithmetic theory.
4532:
4130:
750:
in the late 1970s and continuing through to Microsoft's Spec# system of 2005.
4401:
Proc. 5th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages
167:(and possibly other free variables). Then the following formula is an axiom:(
4491:
4241:
4211:
4178:
4159:
342:
The decision problem for Presburger arithmetic is an interesting example in
299:
233:
4009:
4658:
4621:
4408:
1226:
that defines a set of integers that is not definable using only addition.
4606:. New York, NY, USA: Association for Computing Machinery. pp. 4–13.
4456:
4439:
2017 IEEE 58th Annual Symposium on Foundations of Computer Science (FOCS)
4427:
3894:(1962). "On a Decision Method in Restricted Second Order Arithmetic". In
31:
4585:
Comptes Rendus du I congrès de Mathématiciens des Pays Slaves, Warszawa
4068:
3937:
979:, a relation is Presburger-definable if and only if it is definable in
4353:(Softcover reprint of the original 1st ed. 1976 ed.). Springer.
4695:
Presburger's Article on Integer Arithmetic: Remarks and Translation
4447:
4202:
4000:
42:
of Presburger arithmetic contains only the addition operation and
3910:. Proceedings of the International Congress for Logic. Stanford:
16:
Decidable first-order theory of the natural numbers with addition
4496:(Thesis). Los Angeles: UCLA Electronic Theses and Dissertations
163:
in the language of Presburger arithmetic with a free variable
434:
For a more fine-grained result, let PA(i) be the set of true Σ
92:
In this language, the axioms of Presburger arithmetic are the
307:
The decidability of Presburger arithmetic can be shown using
4552:"A 2 Upper Bound on the Complexity of Presburger Arithmetic"
1186:) are Presburger-definable. Equivalently, for each relation
354:
be the length of a statement in Presburger arithmetic. Then
1752:{\displaystyle (p_{0},\ldots ,p_{d-1})\in \mathbb {N} ^{d}}
765:
A relation is Presburger-definable if and only if it is a
4721:
Interpretations in Presburger Arithmetic (Bachelor Thesis)
3065:{\displaystyle (x_{0},\dots ,x_{d-1})\in \mathbb {N} ^{d}}
2398:{\displaystyle (p_{0},\dots ,p_{d-1})\in \mathbb {Z} ^{d}}
2013:{\displaystyle (x_{0}+p_{0},\dots ,x_{d-1}+p_{d-1})\in S,}
2173:{\displaystyle (x_{0}+p_{0},\dots ,x_{d-1}+p_{d-1})\in R}
268:)". This states that every number is either even or odd.
3629:
3627:
714:
contains a verified quantifier elimination procedure by
4351:
Mathematical Logic (Graduate Texts in Mathematics (37))
4105:"Super-Exponential Complexity of Presburger Arithmetic"
3785:, which fits the restrictions of Presburger arithmetic.
3957:"Theorem Proving in Arithmetic without Multiplication"
2543:{\displaystyle k,x_{0},\dots ,x_{d-1}\in \mathbb {N} }
4493:
The Computational Complexity of Presburger Arithmetic
3955:
Cooper, D.C. (1972). Meltzer, B.; Michie, D. (eds.).
3567:
3547:
3525:
3454:
3387:
3324:
3301:
3281:
3261:
3183:
3161:
3140:
3078:
3005:
2977:
2949:
2921:
2898:
2872:
2833:
2766:
2746:
2559:
2490:
2414:
2338:
2278:
2257:
2235:
2214:
2186:
2090:
2026:
1927:
1863:
1843:
1785:
1765:
1692:
1670:
1628:
1389:
1358:
1332:
1312:
1279:
1244:
1212:
1192:
1172:
1166:(that is, Presburger arithmetic plus a predicate for
1152:
1132:
1100:
1080:
1055:
1035:
1009:
989:
946:
920:
884:
864:
826:
798:
778:
673:
646:
619:
590:
564:
526:
500:
473:
364:
4289:
2014 Formal Methods in Computer-Aided Design (FMCAD)
3773:
is an array of 4 bytes element size, the expression
4747:
A complete Theorem Prover for Presburger Arithmetic
1029:. A relation definable in Büchi arithmetic of base
722:describe an automatic theorem prover that uses the
3753:
3573:
3553:
3531:
3507:
3440:
3370:
3307:
3287:
3267:
3242:
3167:
3146:
3127:
3064:
2991:
2963:
2935:
2904:
2884:
2854:
2810:
2752:
2729:
2542:
2473:
2397:
2322:
2263:
2241:
2220:
2200:
2172:
2076:
2012:
1913:
1849:
1829:
1771:
1751:
1676:
1655:
1611:
1372:
1344:
1318:
1298:
1265:
1218:
1198:
1178:
1158:
1138:
1111:
1086:
1066:
1041:
1021:
995:
964:
932:
906:
870:
850:
812:
784:
706:for Presburger arithmetic exist. For example, the
686:
659:
632:
605:
576:
550:
512:
486:
387:
3830:
3741:
4160:"Semigroups, Presburger Formulas, and Languages"
4057:The Computational Complexity of Logical Theories
3508:{\displaystyle \max(x_{0},\ldots ,x_{d-1})>t}
3455:
3441:{\displaystyle \min(x_{0},\ldots ,x_{d-1})>t}
3388:
4709:Recursion Theory, American Mathematical Society
4059:. Lecture Notes in Mathematics. Vol. 718.
3794:
3275:represents the length of a shift, the integer
2474:{\displaystyle \sum _{i=0}^{d-1}|p_{i}|<s.}
54:axiomatizable; the axioms include a schema of
1656:{\displaystyle R,S\subseteq \mathbb {N} ^{d}}
444:PA(1, j) is in P, while PA(1) is NP-complete.
438:PA statements, and PA(i, j) the set of true Σ
8:
3908:Logic, methodology and philosophy of science
3128:{\displaystyle \sum _{i=0}^{d-1}x_{i}>t,}
2077:{\displaystyle (x_{0},\ldots ,x_{d-1})\in R}
758:Some properties are now given about integer
702:Because Presburger arithmetic is decidable,
355:
78:
4223:"A Survival Guide to Presburger Arithmetic"
3371:{\displaystyle \sum _{i=0}^{d-1}x_{i}>t}
3243:{\displaystyle C(k,(x_{0},\dots ,x_{d-1}))}
2855:{\displaystyle R\subseteq \mathbb {N} ^{d}}
2822:
1914:{\displaystyle (x_{0},\dots ,x_{d-1})\in S}
1266:{\displaystyle R\subseteq \mathbb {N} ^{d}}
719:
446:For i > 0 and j > 2, PA(i + 1, j) is
3705:
3633:
276:
61:Presburger arithmetic is much weaker than
4611:
4590:
4568:
4446:
4387:
4201:
4177:
3999:
3879:
3729:
3693:
3566:
3546:
3524:
3484:
3465:
3453:
3417:
3398:
3386:
3356:
3340:
3329:
3323:
3300:
3280:
3260:
3222:
3203:
3182:
3160:
3139:
3110:
3094:
3083:
3077:
3056:
3052:
3051:
3032:
3013:
3004:
2985:
2984:
2976:
2957:
2956:
2948:
2929:
2928:
2920:
2897:
2871:
2846:
2842:
2841:
2832:
2793:
2774:
2765:
2745:
2710:
2682:
2663:
2644:
2631:
2598:
2579:
2558:
2536:
2535:
2520:
2501:
2489:
2457:
2451:
2442:
2430:
2419:
2413:
2389:
2385:
2384:
2365:
2346:
2337:
2305:
2286:
2277:
2256:
2234:
2213:
2194:
2193:
2185:
2149:
2130:
2111:
2098:
2089:
2053:
2034:
2025:
1986:
1967:
1948:
1935:
1926:
1890:
1871:
1862:
1842:
1812:
1793:
1784:
1764:
1743:
1739:
1738:
1719:
1700:
1691:
1669:
1647:
1643:
1642:
1627:
1580:
1555:
1530:
1511:
1489:
1485:
1484:
1465:
1440:
1421:
1402:
1388:
1366:
1365:
1357:
1331:
1311:
1284:
1278:
1257:
1253:
1252:
1243:
1211:
1191:
1171:
1151:
1131:
1099:
1079:
1054:
1034:
1008:
988:
945:
919:
893:
885:
883:
863:
851:{\displaystyle p\in \mathbb {N} ^{>0}}
839:
835:
834:
825:
806:
805:
797:
777:
678:
672:
651:
645:
624:
618:
589:
584:). Here, 'short' requires bounded (i.e.
563:
542:
531:
525:
499:
478:
472:
374:
369:
363:
217:Presburger arithmetic can be viewed as a
3681:
3618:
2862:is Presburger-definable if and only if:
3842:
3818:
3611:
2323:{\displaystyle (p_{0},\ldots ,p_{d-1})}
3806:
3669:
2811:{\displaystyle (x_{0},\dots ,x_{d-1})}
1830:{\displaystyle (p_{0},\dots ,p_{d-1})}
715:
416:
4432:"Short Presburger Arithmetic is Hard"
4111:. SIAM-AMS Proceedings. Vol. 7.
3717:
3645:
754:Presburger-definable integer relation
409:
7:
4718:Zoethout, Jetze (February 1, 2015).
4291:. Vol. 2014. pp. 139–146.
4029:A mathematical introduction to logic
3862:"The Complexity of Logical Theories"
3657:
3585:accepts a Presburger-definable set.
279:proved Presburger arithmetic to be:
558:complete (and thus NP complete for
3987:Mathematics of Operations Research
1123:integers is Presburger definable.
675:
648:
621:
528:
475:
311:, supplemented by reasoning about
50:operation entirely. The theory is
14:
2992:{\displaystyle t\in \mathbb {N} }
2964:{\displaystyle k\in \mathbb {N} }
2936:{\displaystyle s\in \mathbb {N} }
2201:{\displaystyle s\in \mathbb {N} }
1373:{\displaystyle j\in \mathbb {N} }
813:{\displaystyle t\in \mathbb {N} }
551:{\displaystyle \Sigma _{n-2}^{P}}
38:, who introduced it in 1929. The
4327:Annals of Pure and Applied Logic
3754:King, Barrett & Tinelli 2014
1229:
4512:"Linear Quantifier Elimination"
344:computational complexity theory
4520:Journal of Automated Reasoning
4268:Technische Universität München
4165:Pacific Journal of Mathematics
4055:; Rackoff, Charles W. (1979).
3496:
3458:
3429:
3391:
3237:
3234:
3196:
3187:
3044:
3006:
2805:
2767:
2694:
2624:
2613:
2610:
2572:
2563:
2458:
2443:
2377:
2339:
2317:
2279:
2161:
2091:
2065:
2027:
1998:
1928:
1902:
1864:
1824:
1786:
1731:
1693:
1592:
1504:
1477:
1395:
894:
886:
728:satisfiability modulo theories
600:
594:
328:Gödel's incompleteness theorem
73:of this algorithm is at least
1:
4768:Formal theories of arithmetic
4389:10.1016/S0304-3975(02)00047-6
4113:American Mathematical Society
4107:. In Karp, Richard M. (ed.).
3831:Michaux & Villemaire 1996
3742:Eisenbrand & Shmonin 2008
3295:is the size of the cubes and
4693:Stansifer, Ryan (Sep 1984).
4570:10.1016/0022-0000(78)90021-1
4340:10.1016/0168-0072(95)00022-4
4196:. ACM. pp. 47:1–47:10.
4031:(2nd ed.). Boston, MA:
3881:10.1016/0304-3975(80)90037-7
3867:Theoretical Computer Science
3621:, p. 8, Theorem 1.2.4..
2912:are Presburger-definable and
1121:multiplicatively independent
4370:Muchnik, Andrei A. (2003).
3795:Ginsburg & Spanier 1966
858:such that, for all integer
687:{\displaystyle \Sigma _{2}}
633:{\displaystyle \Sigma _{2}}
487:{\displaystyle \Sigma _{n}}
332:Gentzen's consistency proof
4799:
4593:for an English translation
4297:10.1109/FMCAD.2014.6987606
4027:Enderton, Herbert (2001).
3972:Edinburgh University Press
3561:that holds if and only if
1230:Muchnik's characterization
388:{\displaystyle 2^{2^{cn}}}
356:Fischer & Rabin (1974)
79:Fischer & Rabin (1974)
4773:Logic in computer science
4533:10.1007/s10817-010-9183-0
4490:Nguyen Luu, Dahn (2018).
4221:Haase, Christoph (2018).
4109:Complexity of computation
3912:Stanford University Press
3255:Intuitively, the integer
907:{\displaystyle |n|\geq t}
772:A unary integer relation
720:Nelson & Oppen (1978)
704:automatic theorem provers
4550:Oppen, Derek C. (1978).
4349:Monk, J. Donald (2012).
2740:denote the cube of size
965:{\displaystyle n+p\in R}
748:Stanford Pascal Verifier
712:Isabelle proof assistant
660:{\displaystyle \Pi _{2}}
338:Computational complexity
71:computational complexity
4261:"Presburger Arithmetic"
4242:10.1145/3242953.3242964
4212:10.1145/2603088.2603092
4179:10.2140/pjm.1966.16.285
2760:whose lesser corner is
1299:{\displaystyle x_{i}=j}
1022:{\displaystyle k\geq 2}
494:Presburger Arithmetic (
456:For i>0, PA(i+1) is
313:arithmetical congruence
223:intended interpretation
77:, however, as shown by
4010:10.1287/moor.1080.0320
3767:C programming language
3720:, pp. 47:1-47:10.
3575:
3555:
3533:
3509:
3442:
3381:is replaced either by
3372:
3351:
3309:
3289:
3269:
3244:
3169:
3148:
3129:
3105:
3066:
2993:
2965:
2937:
2906:
2892:then all sections of
2886:
2885:{\displaystyle d>1}
2856:
2812:
2754:
2731:
2544:
2475:
2441:
2399:
2324:
2265:
2243:
2222:
2202:
2174:
2078:
2014:
1915:
1851:
1831:
1773:
1753:
1678:
1657:
1613:
1374:
1346:
1345:{\displaystyle i<d}
1320:
1300:
1273:be a set, the section
1267:
1220:
1200:
1180:
1160:
1140:
1113:
1088:
1068:
1043:
1023:
997:
977:Cobham–Semenov theorem
966:
934:
933:{\displaystyle n\in R}
908:
872:
852:
820:and a positive period
814:
786:
688:
661:
634:
607:
578:
552:
514:
513:{\displaystyle n>2}
488:
425:many-to-one reductions
389:
309:quantifier elimination
4659:10.1145/800133.804361
4622:10.1145/125826.125848
4557:J. Comput. Syst. Sci.
4409:10.1145/512760.512775
3982:Eisenbrand, Friedrich
3845:, pp. 1433–1444.
3777:can be translated to
3730:Nguyen & Pak 2017
3576:
3556:
3534:
3510:
3443:
3373:
3325:
3310:
3290:
3270:
3245:
3170:
3149:
3130:
3079:
3067:
2994:
2966:
2943:such that, for every
2938:
2907:
2887:
2857:
2813:
2755:
2732:
2545:
2476:
2415:
2400:
2325:
2266:
2244:
2223:
2203:
2175:
2079:
2015:
1916:
1852:
1832:
1774:
1754:
1679:
1658:
1614:
1375:
1347:
1321:
1301:
1268:
1221:
1201:
1181:
1161:
1141:
1114:
1089:
1069:
1044:
1024:
998:
967:
935:
909:
873:
853:
815:
787:
746:, beginning with the
730:solvers use complete
689:
662:
635:
608:
579:
553:
515:
489:
390:
20:Presburger arithmetic
4653:. pp. 320–325.
4457:10.1109/FOCS.2017.13
4156:Spanier, Edwin Henry
3964:Machine Intelligence
3926:Math. Systems Theory
3765:For example, in the
3565:
3545:
3523:
3452:
3385:
3322:
3299:
3279:
3259:
3181:
3159:
3138:
3076:
3003:
2975:
2947:
2919:
2896:
2870:
2831:
2764:
2744:
2557:
2488:
2412:
2336:
2276:
2255:
2233:
2212:
2184:
2088:
2024:
1925:
1861:
1841:
1783:
1763:
1690:
1668:
1626:
1387:
1356:
1330:
1310:
1277:
1242:
1210:
1190:
1170:
1150:
1130:
1126:An integer relation
1098:
1078:
1053:
1033:
1007:
987:
944:
918:
882:
862:
824:
796:
776:
671:
644:
617:
606:{\displaystyle O(1)}
588:
562:
524:
498:
471:
395:, for some constant
362:
324:Entscheidungsproblem
34:, named in honor of
4711:. pp. 503–522.
4581:Presburger, Mojżesz
4097:Fischer, Michael J.
3860:Berman, L. (1980).
3833:, pp. 251–277.
3821:, pp. 403–418.
3809:, pp. 186–192.
3797:, pp. 285–296.
3595:Robinson arithmetic
2826: —
732:integer programming
577:{\displaystyle n=3}
547:
161:first-order formula
4763:1929 introductions
4510:Nipkow, T (2010).
4441:. pp. 37–48.
4376:Theor. Comput. Sci
4259:Hoang, Nhat Minh.
4115:. pp. 27–41.
4069:10.1007/BFb0062837
3938:10.1007/BF01746527
3583:automatic sequence
3571:
3551:
3529:
3505:
3438:
3368:
3305:
3285:
3265:
3240:
3165:
3144:
3125:
3062:
2999:such that for all
2989:
2961:
2933:
2902:
2882:
2852:
2824:
2808:
2750:
2727:
2540:
2471:
2395:
2320:
2261:
2239:
2218:
2198:
2170:
2074:
2010:
1911:
1847:
1827:
1769:
1749:
1674:
1653:
1609:
1370:
1342:
1316:
1296:
1263:
1216:
1196:
1176:
1156:
1136:
1112:{\displaystyle k'}
1109:
1084:
1067:{\displaystyle k'}
1064:
1039:
1019:
993:
962:
930:
904:
868:
848:
810:
782:
684:
657:
630:
603:
574:
548:
527:
510:
484:
405:doubly exponential
385:
298:: There exists an
219:first-order theory
96:of the following:
94:universal closures
75:doubly exponential
36:Mojżesz Presburger
24:first-order theory
4749:by Philipp Rümmer
4679:Sibirsk. Mat. Zh.
4466:978-1-5386-3464-6
4306:978-0-9835-6784-4
4152:Ginsburg, Seymour
4122:978-0-8218-1327-0
4101:Rabin, Michael O.
4078:978-3-540-09501-9
4042:978-0-12-238452-3
3892:Büchi, J. Richard
3600:Skolem arithmetic
3574:{\displaystyle R}
3554:{\displaystyle R}
3532:{\displaystyle d}
3308:{\displaystyle t}
3288:{\displaystyle k}
3268:{\displaystyle s}
3168:{\displaystyle s}
3147:{\displaystyle R}
2905:{\displaystyle R}
2823:Muchnik's Theorem
2753:{\displaystyle k}
2264:{\displaystyle S}
2242:{\displaystyle s}
2221:{\displaystyle R}
1850:{\displaystyle S}
1772:{\displaystyle R}
1677:{\displaystyle d}
1319:{\displaystyle R}
1219:{\displaystyle R}
1199:{\displaystyle R}
1179:{\displaystyle R}
1159:{\displaystyle R}
1139:{\displaystyle R}
1087:{\displaystyle k}
1042:{\displaystyle k}
996:{\displaystyle k}
871:{\displaystyle n}
785:{\displaystyle R}
744:computer programs
724:simplex algorithm
277:Presburger (1929)
4790:
4735:
4733:
4732:
4726:
4712:
4701:
4699:
4687:
4670:
4643:
4615:
4591:Stansifer (1984)
4588:
4574:
4572:
4544:
4516:
4504:
4502:
4501:
4484:
4482:
4481:
4450:
4436:
4420:
4393:
4391:
4382:(3): 1433–1444.
4364:
4343:
4318:
4281:
4276:
4274:
4265:
4253:
4227:
4215:
4205:
4191:Proceedings CSL-
4183:
4181:
4145:
4143:
4142:
4133:. Archived from
4090:
4053:Ferrante, Jeanne
4046:
4021:
4003:
3975:
3961:
3949:
3915:
3914:. pp. 1–11.
3885:
3883:
3846:
3840:
3834:
3828:
3822:
3816:
3810:
3804:
3798:
3792:
3786:
3784:
3776:
3772:
3763:
3757:
3751:
3745:
3739:
3733:
3727:
3721:
3715:
3709:
3703:
3697:
3691:
3685:
3679:
3673:
3667:
3661:
3655:
3649:
3643:
3637:
3631:
3622:
3616:
3580:
3578:
3577:
3572:
3560:
3558:
3557:
3552:
3540:
3538:
3536:
3535:
3530:
3514:
3512:
3511:
3506:
3495:
3494:
3470:
3469:
3447:
3445:
3444:
3439:
3428:
3427:
3403:
3402:
3377:
3375:
3374:
3369:
3361:
3360:
3350:
3339:
3314:
3312:
3311:
3306:
3294:
3292:
3291:
3286:
3274:
3272:
3271:
3266:
3249:
3247:
3246:
3241:
3233:
3232:
3208:
3207:
3176:
3174:
3172:
3171:
3166:
3153:
3151:
3150:
3145:
3134:
3132:
3131:
3126:
3115:
3114:
3104:
3093:
3071:
3069:
3068:
3063:
3061:
3060:
3055:
3043:
3042:
3018:
3017:
2998:
2996:
2995:
2990:
2988:
2970:
2968:
2967:
2962:
2960:
2942:
2940:
2939:
2934:
2932:
2911:
2909:
2908:
2903:
2891:
2889:
2888:
2883:
2861:
2859:
2858:
2853:
2851:
2850:
2845:
2827:
2817:
2815:
2814:
2809:
2804:
2803:
2779:
2778:
2759:
2757:
2756:
2751:
2736:
2734:
2733:
2728:
2726:
2722:
2715:
2714:
2693:
2692:
2674:
2673:
2649:
2648:
2636:
2635:
2609:
2608:
2584:
2583:
2549:
2547:
2546:
2541:
2539:
2531:
2530:
2506:
2505:
2480:
2478:
2477:
2472:
2461:
2456:
2455:
2446:
2440:
2429:
2404:
2402:
2401:
2396:
2394:
2393:
2388:
2376:
2375:
2351:
2350:
2331:
2329:
2327:
2326:
2321:
2316:
2315:
2291:
2290:
2270:
2268:
2267:
2262:
2250:
2248:
2246:
2245:
2240:
2227:
2225:
2224:
2219:
2207:
2205:
2204:
2199:
2197:
2179:
2177:
2176:
2171:
2160:
2159:
2141:
2140:
2116:
2115:
2103:
2102:
2083:
2081:
2080:
2075:
2064:
2063:
2039:
2038:
2019:
2017:
2016:
2011:
1997:
1996:
1978:
1977:
1953:
1952:
1940:
1939:
1920:
1918:
1917:
1912:
1901:
1900:
1876:
1875:
1856:
1854:
1853:
1848:
1836:
1834:
1833:
1828:
1823:
1822:
1798:
1797:
1778:
1776:
1775:
1770:
1758:
1756:
1755:
1750:
1748:
1747:
1742:
1730:
1729:
1705:
1704:
1685:
1683:
1681:
1680:
1675:
1662:
1660:
1659:
1654:
1652:
1651:
1646:
1618:
1616:
1615:
1610:
1605:
1601:
1591:
1590:
1566:
1565:
1541:
1540:
1516:
1515:
1500:
1499:
1488:
1476:
1475:
1451:
1450:
1432:
1431:
1407:
1406:
1379:
1377:
1376:
1371:
1369:
1351:
1349:
1348:
1343:
1325:
1323:
1322:
1317:
1305:
1303:
1302:
1297:
1289:
1288:
1272:
1270:
1269:
1264:
1262:
1261:
1256:
1225:
1223:
1222:
1217:
1205:
1203:
1202:
1197:
1185:
1183:
1182:
1177:
1165:
1163:
1162:
1157:
1145:
1143:
1142:
1137:
1118:
1116:
1115:
1110:
1108:
1093:
1091:
1090:
1085:
1073:
1071:
1070:
1065:
1063:
1048:
1046:
1045:
1040:
1028:
1026:
1025:
1020:
1002:
1000:
999:
994:
981:Büchi arithmetic
971:
969:
968:
963:
939:
937:
936:
931:
913:
911:
910:
905:
897:
889:
877:
875:
874:
869:
857:
855:
854:
849:
847:
846:
838:
819:
817:
816:
811:
809:
791:
789:
788:
783:
693:
691:
690:
685:
683:
682:
666:
664:
663:
658:
656:
655:
639:
637:
636:
631:
629:
628:
612:
610:
609:
604:
583:
581:
580:
575:
557:
555:
554:
549:
546:
541:
519:
517:
516:
511:
493:
491:
490:
485:
483:
482:
429:Peano arithmetic
421:TimeAlternations
394:
392:
391:
386:
384:
383:
382:
381:
320:Peano arithmetic
67:decidable theory
63:Peano arithmetic
4798:
4797:
4793:
4792:
4791:
4789:
4788:
4787:
4753:
4752:
4743:
4738:
4730:
4728:
4724:
4717:
4706:
4697:
4692:
4675:
4648:
4632:
4598:
4579:
4549:
4514:
4509:
4499:
4497:
4489:
4479:
4477:
4467:
4434:
4426:Nguyen, Danny;
4425:
4398:
4369:
4361:
4348:
4323:
4307:
4286:
4272:
4270:
4263:
4258:
4230:ACM SIGLOG News
4225:
4220:
4188:
4150:
4140:
4138:
4123:
4095:
4079:
4061:Springer-Verlag
4051:
4043:
4026:
3980:
3959:
3954:
3920:
3900:Suppes, Patrick
3890:
3859:
3855:
3850:
3849:
3841:
3837:
3829:
3825:
3817:
3813:
3805:
3801:
3793:
3789:
3782:
3778:
3774:
3770:
3764:
3760:
3752:
3748:
3740:
3736:
3728:
3724:
3716:
3712:
3706:Nguyen Luu 2018
3704:
3700:
3692:
3688:
3680:
3676:
3668:
3664:
3656:
3652:
3644:
3640:
3634:Presburger 1929
3632:
3625:
3617:
3613:
3608:
3591:
3563:
3562:
3543:
3542:
3521:
3520:
3519:
3480:
3461:
3450:
3449:
3413:
3394:
3383:
3382:
3352:
3320:
3319:
3297:
3296:
3277:
3276:
3257:
3256:
3253:
3218:
3199:
3179:
3178:
3157:
3156:
3155:
3136:
3135:
3106:
3074:
3073:
3050:
3028:
3009:
3001:
3000:
2973:
2972:
2971:, there exists
2945:
2944:
2917:
2916:
2894:
2893:
2868:
2867:
2840:
2829:
2828:
2825:
2789:
2770:
2762:
2761:
2742:
2741:
2706:
2678:
2659:
2640:
2627:
2623:
2619:
2594:
2575:
2555:
2554:
2516:
2497:
2486:
2485:
2447:
2410:
2409:
2383:
2361:
2342:
2334:
2333:
2301:
2282:
2274:
2273:
2272:
2253:
2252:
2231:
2230:
2229:
2210:
2209:
2182:
2181:
2145:
2126:
2107:
2094:
2086:
2085:
2084:if and only if
2049:
2030:
2022:
2021:
1982:
1963:
1944:
1931:
1923:
1922:
1886:
1867:
1859:
1858:
1839:
1838:
1808:
1789:
1781:
1780:
1761:
1760:
1737:
1715:
1696:
1688:
1687:
1666:
1665:
1664:
1641:
1624:
1623:
1622:Given two sets
1576:
1551:
1526:
1507:
1483:
1461:
1436:
1417:
1398:
1394:
1390:
1385:
1384:
1380:is defined as
1354:
1353:
1328:
1327:
1308:
1307:
1280:
1275:
1274:
1251:
1240:
1239:
1232:
1208:
1207:
1188:
1187:
1168:
1167:
1148:
1147:
1128:
1127:
1101:
1096:
1095:
1076:
1075:
1056:
1051:
1050:
1031:
1030:
1005:
1004:
985:
984:
942:
941:
940:if and only if
916:
915:
880:
879:
860:
859:
833:
822:
821:
794:
793:
774:
773:
756:
700:
674:
669:
668:
647:
642:
641:
620:
615:
614:
586:
585:
560:
559:
522:
521:
496:
495:
474:
469:
468:
461:
455:
451:
445:
443:
441:
437:
370:
365:
360:
359:
340:
274:
240:, there exists
87:
46:, omitting the
28:natural numbers
17:
12:
11:
5:
4796:
4794:
4786:
4785:
4780:
4775:
4770:
4765:
4755:
4754:
4751:
4750:
4742:
4741:External links
4739:
4737:
4736:
4714:
4713:
4703:
4702:
4689:
4688:
4682:(in Russian).
4672:
4671:
4645:
4644:
4630:
4613:10.1.1.37.1995
4595:
4594:
4576:
4575:
4563:(3): 323–332.
4546:
4545:
4527:(2): 189–212.
4506:
4505:
4486:
4485:
4465:
4422:
4421:
4395:
4394:
4366:
4365:
4359:
4345:
4344:
4334:(3): 251–277.
4320:
4319:
4305:
4283:
4282:
4255:
4254:
4217:
4216:
4185:
4184:
4172:(2): 285–296.
4147:
4146:
4121:
4092:
4091:
4077:
4048:
4047:
4041:
4033:Academic Press
4023:
4022:
3994:(4): 839–850.
3977:
3976:
3951:
3950:
3932:(2): 186–192.
3917:
3916:
3904:Tarski, Alfred
3887:
3886:
3856:
3854:
3851:
3848:
3847:
3835:
3823:
3811:
3799:
3787:
3780:
3758:
3746:
3734:
3722:
3710:
3698:
3694:Stansifer 1984
3686:
3684:, p. 188.
3674:
3662:
3660:, p. 240.
3650:
3638:
3623:
3610:
3609:
3607:
3604:
3603:
3602:
3597:
3590:
3587:
3570:
3550:
3528:
3504:
3501:
3498:
3493:
3490:
3487:
3483:
3479:
3476:
3473:
3468:
3464:
3460:
3457:
3437:
3434:
3431:
3426:
3423:
3420:
3416:
3412:
3409:
3406:
3401:
3397:
3393:
3390:
3379:
3378:
3367:
3364:
3359:
3355:
3349:
3346:
3343:
3338:
3335:
3332:
3328:
3304:
3284:
3264:
3252:
3251:
3239:
3236:
3231:
3228:
3225:
3221:
3217:
3214:
3211:
3206:
3202:
3198:
3195:
3192:
3189:
3186:
3164:
3143:
3124:
3121:
3118:
3113:
3109:
3103:
3100:
3097:
3092:
3089:
3086:
3082:
3059:
3054:
3049:
3046:
3041:
3038:
3035:
3031:
3027:
3024:
3021:
3016:
3012:
3008:
2987:
2983:
2980:
2959:
2955:
2952:
2931:
2927:
2924:
2913:
2901:
2881:
2878:
2875:
2849:
2844:
2839:
2836:
2820:
2807:
2802:
2799:
2796:
2792:
2788:
2785:
2782:
2777:
2773:
2769:
2749:
2738:
2737:
2725:
2721:
2718:
2713:
2709:
2705:
2702:
2699:
2696:
2691:
2688:
2685:
2681:
2677:
2672:
2669:
2666:
2662:
2658:
2655:
2652:
2647:
2643:
2639:
2634:
2630:
2626:
2622:
2618:
2615:
2612:
2607:
2604:
2601:
2597:
2593:
2590:
2587:
2582:
2578:
2574:
2571:
2568:
2565:
2562:
2538:
2534:
2529:
2526:
2523:
2519:
2515:
2512:
2509:
2504:
2500:
2496:
2493:
2482:
2481:
2470:
2467:
2464:
2460:
2454:
2450:
2445:
2439:
2436:
2433:
2428:
2425:
2422:
2418:
2392:
2387:
2382:
2379:
2374:
2371:
2368:
2364:
2360:
2357:
2354:
2349:
2345:
2341:
2319:
2314:
2311:
2308:
2304:
2300:
2297:
2294:
2289:
2285:
2281:
2260:
2238:
2228:is said to be
2217:
2196:
2192:
2189:
2169:
2166:
2163:
2158:
2155:
2152:
2148:
2144:
2139:
2136:
2133:
2129:
2125:
2122:
2119:
2114:
2110:
2106:
2101:
2097:
2093:
2073:
2070:
2067:
2062:
2059:
2056:
2052:
2048:
2045:
2042:
2037:
2033:
2029:
2009:
2006:
2003:
2000:
1995:
1992:
1989:
1985:
1981:
1976:
1973:
1970:
1966:
1962:
1959:
1956:
1951:
1947:
1943:
1938:
1934:
1930:
1910:
1907:
1904:
1899:
1896:
1893:
1889:
1885:
1882:
1879:
1874:
1870:
1866:
1846:
1826:
1821:
1818:
1815:
1811:
1807:
1804:
1801:
1796:
1792:
1788:
1768:
1746:
1741:
1736:
1733:
1728:
1725:
1722:
1718:
1714:
1711:
1708:
1703:
1699:
1695:
1673:
1650:
1645:
1640:
1637:
1634:
1631:
1620:
1619:
1608:
1604:
1600:
1597:
1594:
1589:
1586:
1583:
1579:
1575:
1572:
1569:
1564:
1561:
1558:
1554:
1550:
1547:
1544:
1539:
1536:
1533:
1529:
1525:
1522:
1519:
1514:
1510:
1506:
1503:
1498:
1495:
1492:
1487:
1482:
1479:
1474:
1471:
1468:
1464:
1460:
1457:
1454:
1449:
1446:
1443:
1439:
1435:
1430:
1427:
1424:
1420:
1416:
1413:
1410:
1405:
1401:
1397:
1393:
1368:
1364:
1361:
1341:
1338:
1335:
1315:
1295:
1292:
1287:
1283:
1260:
1255:
1250:
1247:
1231:
1228:
1215:
1195:
1175:
1155:
1135:
1107:
1104:
1083:
1062:
1059:
1038:
1018:
1015:
1012:
992:
961:
958:
955:
952:
949:
929:
926:
923:
903:
900:
896:
892:
888:
867:
845:
842:
837:
832:
829:
808:
804:
801:
781:
767:semilinear set
755:
752:
699:
696:
681:
677:
654:
650:
627:
623:
602:
599:
596:
593:
573:
570:
567:
545:
540:
537:
534:
530:
509:
506:
503:
481:
477:
459:
449:
439:
435:
380:
377:
373:
368:
339:
336:
305:
304:
293:
287:
273:
270:
204:
203:
149:
131:
122:
105:
86:
83:
48:multiplication
15:
13:
10:
9:
6:
4:
3:
2:
4795:
4784:
4781:
4779:
4776:
4774:
4771:
4769:
4766:
4764:
4761:
4760:
4758:
4748:
4745:
4744:
4740:
4723:
4722:
4716:
4715:
4710:
4705:
4704:
4696:
4691:
4690:
4685:
4681:
4680:
4674:
4673:
4668:
4664:
4660:
4656:
4652:
4647:
4646:
4641:
4637:
4633:
4627:
4623:
4619:
4614:
4609:
4605:
4601:
4600:Pugh, William
4597:
4596:
4592:
4586:
4582:
4578:
4577:
4571:
4566:
4562:
4559:
4558:
4553:
4548:
4547:
4542:
4538:
4534:
4530:
4526:
4522:
4521:
4513:
4508:
4507:
4495:
4494:
4488:
4487:
4476:
4472:
4468:
4462:
4458:
4454:
4449:
4444:
4440:
4433:
4429:
4424:
4423:
4418:
4414:
4410:
4406:
4402:
4397:
4396:
4390:
4385:
4381:
4377:
4373:
4368:
4367:
4362:
4360:9781468494549
4356:
4352:
4347:
4346:
4341:
4337:
4333:
4329:
4328:
4322:
4321:
4316:
4312:
4308:
4302:
4298:
4294:
4290:
4285:
4284:
4280:
4269:
4262:
4257:
4256:
4251:
4247:
4243:
4239:
4235:
4231:
4224:
4219:
4218:
4213:
4209:
4204:
4199:
4195:
4194:
4187:
4186:
4180:
4175:
4171:
4167:
4166:
4161:
4157:
4153:
4149:
4148:
4137:on 2006-09-15
4136:
4132:
4128:
4124:
4118:
4114:
4110:
4106:
4102:
4098:
4094:
4093:
4088:
4084:
4080:
4074:
4070:
4066:
4062:
4058:
4054:
4050:
4049:
4044:
4038:
4034:
4030:
4025:
4024:
4019:
4015:
4011:
4007:
4002:
3997:
3993:
3989:
3988:
3983:
3979:
3978:
3973:
3969:
3965:
3958:
3953:
3952:
3947:
3943:
3939:
3935:
3931:
3927:
3923:
3919:
3918:
3913:
3909:
3905:
3901:
3897:
3896:Nagel, Ernest
3893:
3889:
3888:
3882:
3877:
3873:
3869:
3868:
3863:
3858:
3857:
3852:
3844:
3839:
3836:
3832:
3827:
3824:
3820:
3815:
3812:
3808:
3803:
3800:
3796:
3791:
3788:
3768:
3762:
3759:
3755:
3750:
3747:
3743:
3738:
3735:
3731:
3726:
3723:
3719:
3714:
3711:
3707:
3702:
3699:
3695:
3690:
3687:
3683:
3682:Enderton 2001
3678:
3675:
3671:
3666:
3663:
3659:
3654:
3651:
3647:
3642:
3639:
3635:
3630:
3628:
3624:
3620:
3619:Zoethout 2015
3615:
3612:
3605:
3601:
3598:
3596:
3593:
3592:
3588:
3586:
3584:
3568:
3548:
3526:
3516:
3502:
3499:
3491:
3488:
3485:
3481:
3477:
3474:
3471:
3466:
3462:
3435:
3432:
3424:
3421:
3418:
3414:
3410:
3407:
3404:
3399:
3395:
3365:
3362:
3357:
3353:
3347:
3344:
3341:
3336:
3333:
3330:
3326:
3318:
3317:
3316:
3302:
3282:
3262:
3229:
3226:
3223:
3219:
3215:
3212:
3209:
3204:
3200:
3193:
3190:
3184:
3162:
3141:
3122:
3119:
3116:
3111:
3107:
3101:
3098:
3095:
3090:
3087:
3084:
3080:
3057:
3047:
3039:
3036:
3033:
3029:
3025:
3022:
3019:
3014:
3010:
2981:
2978:
2953:
2950:
2925:
2922:
2915:there exists
2914:
2899:
2879:
2876:
2873:
2865:
2864:
2863:
2847:
2837:
2834:
2819:
2800:
2797:
2794:
2790:
2786:
2783:
2780:
2775:
2771:
2747:
2723:
2719:
2716:
2711:
2707:
2703:
2700:
2697:
2689:
2686:
2683:
2679:
2675:
2670:
2667:
2664:
2660:
2656:
2653:
2650:
2645:
2641:
2637:
2632:
2628:
2620:
2616:
2605:
2602:
2599:
2595:
2591:
2588:
2585:
2580:
2576:
2569:
2566:
2560:
2553:
2552:
2551:
2532:
2527:
2524:
2521:
2517:
2513:
2510:
2507:
2502:
2498:
2494:
2491:
2484:Finally, for
2468:
2465:
2462:
2452:
2448:
2437:
2434:
2431:
2426:
2423:
2420:
2416:
2408:
2407:
2406:
2390:
2380:
2372:
2369:
2366:
2362:
2358:
2355:
2352:
2347:
2343:
2312:
2309:
2306:
2302:
2298:
2295:
2292:
2287:
2283:
2258:
2236:
2215:
2190:
2187:
2167:
2164:
2156:
2153:
2150:
2146:
2142:
2137:
2134:
2131:
2127:
2123:
2120:
2117:
2112:
2108:
2104:
2099:
2095:
2071:
2068:
2060:
2057:
2054:
2050:
2046:
2043:
2040:
2035:
2031:
2007:
2004:
2001:
1993:
1990:
1987:
1983:
1979:
1974:
1971:
1968:
1964:
1960:
1957:
1954:
1949:
1945:
1941:
1936:
1932:
1908:
1905:
1897:
1894:
1891:
1887:
1883:
1880:
1877:
1872:
1868:
1844:
1837:-periodic in
1819:
1816:
1813:
1809:
1805:
1802:
1799:
1794:
1790:
1766:
1744:
1734:
1726:
1723:
1720:
1716:
1712:
1709:
1706:
1701:
1697:
1671:
1648:
1638:
1635:
1632:
1629:
1606:
1602:
1598:
1595:
1587:
1584:
1581:
1577:
1573:
1570:
1567:
1562:
1559:
1556:
1552:
1548:
1545:
1542:
1537:
1534:
1531:
1527:
1523:
1520:
1517:
1512:
1508:
1501:
1496:
1493:
1490:
1480:
1472:
1469:
1466:
1462:
1458:
1455:
1452:
1447:
1444:
1441:
1437:
1433:
1428:
1425:
1422:
1418:
1414:
1411:
1408:
1403:
1399:
1391:
1383:
1382:
1381:
1362:
1359:
1339:
1336:
1333:
1313:
1293:
1290:
1285:
1281:
1258:
1248:
1245:
1236:
1227:
1213:
1193:
1173:
1153:
1133:
1124:
1122:
1105:
1102:
1081:
1060:
1057:
1036:
1016:
1013:
1010:
990:
982:
978:
973:
959:
956:
953:
950:
947:
927:
924:
921:
901:
898:
890:
865:
843:
840:
830:
827:
802:
799:
779:
770:
768:
763:
761:
753:
751:
749:
745:
741:
735:
733:
729:
725:
721:
717:
716:Nipkow (2010)
713:
709:
705:
697:
695:
679:
652:
625:
597:
591:
571:
568:
565:
543:
538:
535:
532:
507:
504:
501:
479:
465:
463:
453:
432:
430:
426:
422:
418:
417:Berman (1980)
413:
411:
406:
402:
398:
378:
375:
371:
366:
357:
353:
349:
345:
337:
335:
333:
329:
325:
321:
318:In contrast,
316:
314:
310:
301:
297:
294:
291:
288:
285:
282:
281:
280:
278:
271:
269:
267:
263:
259:
255:
251:
247:
243:
239:
235:
231:
226:
224:
220:
215:
213:
209:
201:
197:
194:
190:
186:
182:
178:
174:
171:(0) ∧ ∀
170:
166:
162:
158:
154:
150:
147:
143:
139:
135:
132:
130:
126:
123:
121:
117:
113:
109:
106:
103:
99:
98:
97:
95:
90:
84:
82:
80:
76:
72:
68:
64:
59:
57:
53:
49:
45:
41:
37:
33:
29:
25:
21:
4783:Model theory
4778:Proof theory
4729:. Retrieved
4720:
4708:
4683:
4677:
4650:
4603:
4584:
4560:
4555:
4524:
4518:
4498:. Retrieved
4492:
4478:. Retrieved
4438:
4400:
4379:
4375:
4350:
4331:
4325:
4288:
4278:
4271:. Retrieved
4236:(3): 67–82.
4233:
4229:
4190:
4169:
4163:
4139:. Retrieved
4135:the original
4108:
4056:
4028:
3991:
3985:
3967:
3963:
3929:
3925:
3922:Cobham, Alan
3907:
3874:(1): 71–77.
3871:
3865:
3853:Bibliography
3843:Muchnik 2003
3838:
3826:
3819:Semenov 1977
3814:
3802:
3790:
3761:
3749:
3737:
3725:
3713:
3708:, chapter 3.
3701:
3689:
3677:
3665:
3653:
3641:
3614:
3517:
3380:
3254:
2821:
2739:
2483:
2405:such that
1857:if, for all
1686:of integers
1621:
1237:
1233:
1125:
974:
771:
764:
757:
742:systems for
736:
701:
698:Applications
466:
433:
414:
410:Oppen (1978)
400:
396:
351:
341:
317:
306:
275:
265:
261:
257:
253:
249:
245:
241:
237:
230:divisibility
227:
216:
208:axiom schema
205:
199:
195:
192:
188:
184:
180:
176:
172:
168:
164:
156:
152:
145:
141:
137:
133:
128:
124:
119:
115:
111:
107:
101:
91:
88:
60:
19:
18:
4403:: 141–150.
3807:Cobham 1969
3670:Nipkow 2010
2208:, the set
740:correctness
348:computation
303:equivalent.
4757:Categories
4731:2023-08-25
4686:: 403–418.
4631:0897914597
4500:2022-09-08
4480:2022-09-04
4448:1708.08179
4141:2006-06-11
4131:1205569621
3718:Haase 2014
3646:Büchi 1962
3606:References
3541:predicate
1921:such that
1779:is called
1759:, the set
878:such that
667:(and thus
403:that have
284:consistent
272:Properties
206:(5) is an
191:+ 1))) → ∀
52:computably
4608:CiteSeerX
4587:: 92–101.
4428:Pak, Igor
4203:1401.5266
4001:0801.4336
3658:Monk 2012
3489:−
3475:…
3422:−
3408:…
3345:−
3327:∑
3227:−
3213:…
3175:-periodic
3099:−
3081:∑
3048:∈
3037:−
3023:…
2982:∈
2954:∈
2926:∈
2838:⊆
2798:−
2784:…
2704:≤
2698:∣
2687:−
2668:−
2654:…
2603:−
2589:…
2533:∈
2525:−
2511:…
2435:−
2417:∑
2381:∈
2370:−
2356:…
2332:for some
2330:-periodic
2310:−
2296:…
2271:if it is
2249:-periodic
2191:∈
2165:∈
2154:−
2135:−
2121:…
2069:∈
2058:−
2044:…
2002:∈
1991:−
1972:−
1958:…
1906:∈
1895:−
1881:…
1817:−
1803:…
1735:∈
1724:−
1710:…
1639:⊆
1596:∈
1585:−
1571:…
1535:−
1521:…
1502:∣
1494:−
1481:∈
1470:−
1456:…
1426:−
1412:…
1363:∈
1249:⊆
1014:≥
957:∈
925:∈
899:≥
831:∈
803:∈
760:relations
738:proof-of-
676:Σ
649:Π
622:Σ
536:−
529:Σ
476:Σ
462:-complete
452:-complete
300:algorithm
296:decidable
244: : (
234:primality
212:induction
56:induction
40:signature
4727:(Thesis)
4667:13966721
4541:14279141
4430:(2017).
4273:22 March
4250:51847374
4158:(1966).
4103:(1974).
4018:15698556
3974:: 91–99.
3946:19792434
3906:(eds.).
3783:+i+i+i+i
3589:See also
1106:′
1061:′
1003:for all
983:of base
290:complete
140:+ 1) = (
85:Overview
44:equality
32:addition
4640:3174094
4475:3425421
4417:6342372
4315:5542629
4087:0537764
3781:baseadr
975:By the
159:) be a
26:of the
22:is the
4665:
4638:
4628:
4610:
4589:, see
4539:
4473:
4463:
4415:
4357:
4313:
4303:
4248:
4129:
4119:
4085:
4075:
4039:
4016:
3944:
3448:or by
2180:. For
1684:-tuple
1663:and a
1326:, for
1119:being
467:Short
350:. Let
264:+ 1 =
127:+ 0 =
114:+ 1 →
110:+ 1 =
100:¬(0 =
4725:(PDF)
4698:(PDF)
4663:S2CID
4636:S2CID
4537:S2CID
4515:(PDF)
4471:S2CID
4443:arXiv
4435:(PDF)
4413:S2CID
4311:S2CID
4264:(PDF)
4246:S2CID
4226:(PDF)
4198:arXiv
4014:S2CID
3996:arXiv
3960:(PDF)
3942:S2CID
3769:, if
3072:with
2550:let
2020:then
520:) is
326:. By
256:) ∨ (
148:) + 1
30:with
4626:ISBN
4461:ISBN
4355:ISBN
4301:ISBN
4275:2024
4193:LICS
4127:OCLC
4117:ISBN
4073:ISBN
4037:ISBN
3539:-ary
3500:>
3433:>
3363:>
3117:>
2877:>
2717:<
2463:<
1352:and
1337:<
1238:Let
1094:and
1074:for
1049:and
841:>
505:>
346:and
183:) →
151:Let
104:+ 1)
4655:doi
4618:doi
4565:doi
4529:doi
4453:doi
4405:doi
4384:doi
4380:290
4336:doi
4293:doi
4238:doi
4208:doi
4174:doi
4065:doi
4006:doi
3934:doi
3876:doi
3456:max
3389:min
3177:in
3154:is
2866:if
2251:in
1306:of
708:Coq
431:.)
334:).
232:or
210:of
136:+ (
4759::
4684:18
4661:.
4634:.
4624:.
4616:.
4561:16
4554:.
4535:.
4525:45
4523:.
4517:.
4469:.
4459:.
4451:.
4437:.
4411:.
4378:.
4374:.
4332:77
4330:.
4309:.
4299:.
4277:.
4266:.
4244:.
4232:.
4228:.
4206:.
4170:16
4168:.
4162:.
4154:;
4125:.
4099:;
4083:MR
4081:.
4071:.
4063:.
4035:.
4012:.
4004:.
3992:33
3990:.
3970:.
3966:.
3962:.
3940:.
3928:.
3902:;
3898:;
3872:11
3870:.
3864:.
3626:^
3515:.
2818:.
972:.
914:,
769:.
464:.
412:.
260:+
252:=
248:+
202:).
144:+
118:=
81:.
58:.
4734:.
4669:.
4657::
4642:.
4620::
4573:.
4567::
4543:.
4531::
4503:.
4483:.
4455::
4445::
4419:.
4407::
4392:.
4386::
4363:.
4342:.
4338::
4317:.
4295::
4252:.
4240::
4234:5
4214:.
4210::
4200::
4182:.
4176::
4144:.
4089:.
4067::
4045:.
4020:.
4008::
3998::
3968:7
3948:.
3936::
3930:3
3884:.
3878::
3779:a
3775:a
3771:a
3756:.
3744:.
3732:.
3696:.
3672:.
3648:.
3636:.
3569:R
3549:R
3527:d
3503:t
3497:)
3492:1
3486:d
3482:x
3478:,
3472:,
3467:0
3463:x
3459:(
3436:t
3430:)
3425:1
3419:d
3415:x
3411:,
3405:,
3400:0
3396:x
3392:(
3366:t
3358:i
3354:x
3348:1
3342:d
3337:0
3334:=
3331:i
3303:t
3283:k
3263:s
3250:.
3238:)
3235:)
3230:1
3224:d
3220:x
3216:,
3210:,
3205:0
3201:x
3197:(
3194:,
3191:k
3188:(
3185:C
3163:s
3142:R
3123:,
3120:t
3112:i
3108:x
3102:1
3096:d
3091:0
3088:=
3085:i
3058:d
3053:N
3045:)
3040:1
3034:d
3030:x
3026:,
3020:,
3015:0
3011:x
3007:(
2986:N
2979:t
2958:N
2951:k
2930:N
2923:s
2900:R
2880:1
2874:d
2848:d
2843:N
2835:R
2806:)
2801:1
2795:d
2791:x
2787:,
2781:,
2776:0
2772:x
2768:(
2748:k
2724:}
2720:k
2712:i
2708:c
2701:0
2695:)
2690:1
2684:d
2680:c
2676:+
2671:1
2665:d
2661:x
2657:,
2651:,
2646:0
2642:c
2638:+
2633:0
2629:x
2625:(
2621:{
2617:=
2614:)
2611:)
2606:1
2600:d
2596:x
2592:,
2586:,
2581:0
2577:x
2573:(
2570:,
2567:k
2564:(
2561:C
2537:N
2528:1
2522:d
2518:x
2514:,
2508:,
2503:0
2499:x
2495:,
2492:k
2469:.
2466:s
2459:|
2453:i
2449:p
2444:|
2438:1
2432:d
2427:0
2424:=
2421:i
2391:d
2386:Z
2378:)
2373:1
2367:d
2363:p
2359:,
2353:,
2348:0
2344:p
2340:(
2318:)
2313:1
2307:d
2303:p
2299:,
2293:,
2288:0
2284:p
2280:(
2259:S
2237:s
2216:R
2195:N
2188:s
2168:R
2162:)
2157:1
2151:d
2147:p
2143:+
2138:1
2132:d
2128:x
2124:,
2118:,
2113:0
2109:p
2105:+
2100:0
2096:x
2092:(
2072:R
2066:)
2061:1
2055:d
2051:x
2047:,
2041:,
2036:0
2032:x
2028:(
2008:,
2005:S
1999:)
1994:1
1988:d
1984:p
1980:+
1975:1
1969:d
1965:x
1961:,
1955:,
1950:0
1946:p
1942:+
1937:0
1933:x
1929:(
1909:S
1903:)
1898:1
1892:d
1888:x
1884:,
1878:,
1873:0
1869:x
1865:(
1845:S
1825:)
1820:1
1814:d
1810:p
1806:,
1800:,
1795:0
1791:p
1787:(
1767:R
1745:d
1740:N
1732:)
1727:1
1721:d
1717:p
1713:,
1707:,
1702:0
1698:p
1694:(
1672:d
1649:d
1644:N
1636:S
1633:,
1630:R
1607:.
1603:}
1599:R
1593:)
1588:1
1582:d
1578:x
1574:,
1568:,
1563:1
1560:+
1557:i
1553:x
1549:,
1546:j
1543:,
1538:1
1532:i
1528:x
1524:,
1518:,
1513:0
1509:x
1505:(
1497:1
1491:d
1486:N
1478:)
1473:1
1467:d
1463:x
1459:,
1453:,
1448:1
1445:+
1442:i
1438:x
1434:,
1429:1
1423:i
1419:x
1415:,
1409:,
1404:0
1400:x
1396:(
1392:{
1367:N
1360:j
1340:d
1334:i
1314:R
1294:j
1291:=
1286:i
1282:x
1259:d
1254:N
1246:R
1214:R
1194:R
1174:R
1154:R
1134:R
1103:k
1082:k
1058:k
1037:k
1017:2
1011:k
991:k
960:R
954:p
951:+
948:n
928:R
922:n
902:t
895:|
891:n
887:|
866:n
844:0
836:N
828:p
807:N
800:t
780:R
680:2
653:2
626:2
601:)
598:1
595:(
592:O
572:3
569:=
566:n
544:P
539:2
533:n
508:2
502:n
480:n
460:i
458:Σ
450:i
448:Σ
440:i
436:i
401:n
397:c
379:n
376:c
372:2
367:2
352:n
266:x
262:y
258:y
254:x
250:y
246:y
242:y
238:x
200:y
198:(
196:P
193:y
189:x
187:(
185:P
181:x
179:(
177:P
175:(
173:x
169:P
165:x
157:x
155:(
153:P
146:y
142:x
138:y
134:x
129:x
125:x
120:y
116:x
112:y
108:x
102:x
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.