Talk:Presburger arithmetic

From Wikipedia, the free encyclopedia

has at least a runtime of 2^(2^(cn)) for some constant c. Here, n is the length of the Presburger statement. Hence, the problem is one of the few that provably need more than polynomial run time.

You mean more than polynomial or more than exponential ? --Taw

Both. But "polynomial time" P is a pretty important class of problems, and this is one of the few problems that can be shown not to be in there, so that's why I explicitly mentioned polynomial time. --AxelBoldt

I know just a little of mathematics but I don't see clearly the meaning of the last theorem... ∀ x ∀ y : ( (? z : x + z = y + 1) ? (∀ z : ¬ (((1 + y) + 1) + z = x) ) ) May be the last part of it is " = z + x " instead of " + z = x ". --jimmer_lactic

Working from the inside out of (∀ z : ¬ (((1 + y) + 1) + z = x) ):

1. ((1 + y) + 1) means y+2;
2. (((1 + y) + 1) + z = x) means that z (a non-negative integer) can be added to y+2 to make x;
3. (∀ z : ¬ (((1 + y) + 1) + z = x) ) means that for any non-negative integer, it cannot be added to y+2 to make x, so y+2 must be strictly greater than x. --Henrygb 23:28, 31 Jan 2005 (UTC)

The confusion actually arises when you don't notice that the two z's are separately quantified. The z on the left of implication is not the same as the z on the right. -- jaywalker

I can see jaywalkers point, but why would this then mean 'This sentence states that if x≤y+1, then y+2>x.'? I'd say it means, 'if x+A=y+1 then not(y+2+B=x)', where A and B are the respective z's. Of course this cannot be proven, since its not a true statement, at least over the naturals. Have I got something severly wrong here? --Wintifax

Sorry, I just got it, it actually does mean what it says it should mean and of course the statement is true. So, if Presburger is decidalbe, why can this result not be shown? I still think something's wrong here. -- Wintifax

"and in fact completeness for it is false; this is the content of Gödel's incompleteness theorem."  : I don't think this is quite true. The latter theorem states only that the axioms of Peano arithmetic are either inconsistent or incomplete. It would be nice if we knew that the axioms were consistent (and therefore that arithmetic was incomplete), but there is still a possibility of inconsistency. Disclaimer: I am not a logician. -Mike

[edit] On not requiring exponential run time

As it turns out, it doesn't require exponential run time to decide a proposition expressed in Presberger arithmetic. The classic proof is correct, but illusory.

First, in G. Nelson and D. C. Oppen, "Fast decision procedures based on congruence closure". J. ACM, 27(2):356-364, Apr. 1980., Oppen and Nelson describe an automatic theorem prover which uses the simplex algorithm to decide the arithmetic portion of the problem. (This approach is the basis of about five proof-of-correctness systems, beginning with the Stanford Pascal Verifier and continuing though to Microsoft's new Spec# system.)

The simplex algorithm does indeed have exponential worst-case run time. But the average run time is far better. In fact, exponential run time is only observed for specially constructed cases designed to force the algorithm to visit every vertex of the polytope.

For a deterministic algorithm, such a specially constructed worst case is possible. But if the algorthm is made non-deterministic, so that the order in which the vertices are explored has some randomness, it is no longer possible to reliably force the pathological case. There's a whole family of NP-hard problems that yield to this approach.

The classic proof assumes determinism, but most writings on the subject don't mention that.

On a side note, Presberger arithmetic can be extended to include multiplication by constants (it's just multiple additions, right?), which makes it much more useful for proof of correctness work. Most subscript calculations then fall within the region of decidable problems. --Nagle 22:17, 13 March 2006 (UTC)

Simplex algorithm in the classical Nelson--Oppen and other theorem provers does not solve “extended Presburger arithmetic”. It solves only the quantifier-free case (although extended with <=). In fact, less than that, because arbitrary propositional conjunctions are not considered: It can decide whether a conjunction of equalities (=), ineqaulity (<=) and disequalities (!=) of terms with addition is satisfiable. If you combine simplex, a decision procedure for equality, and a SAT solver, you obtain an exponential algorithm, but still only for quantifier-free theory of addition with inequalities. Algorithms for Presburger arithmetic can decide formulas with quantifiers, and this is what causes the superexponential complexity. However, as Bundy notes, the quantifier-free subcase is sufficient for program verification (A survey of automated deduction, p. 9).

BTW, you probably meant to cite Nelson--Oppen's A simplifier based on efficient decision algorithms, Proc. 5th ACM SIGACT-SIGPLAN POPL, 1978. The reference you have given (Fast decision procedures based on congruence closure) deals only with equality and LISP lists.

--158.195.89.69 17:00, 4 July 2006 (UTC) Jan Kluka (first name dot last name at gmail dot com)

You're right; I cited the wrong paper. And, of course, if you extend Presburger arithmetic to incldue nested quantifiers, the complexity goes up. --John Nagle 17:10, 4 July 2006 (UTC)

Well, Presburger arithmetic is defined to include nested quantifier, it is not an extension (the example at the end of the first section correctly points that out by containing some quantifiers). People usually say linear arithmetic if they mean the quantifier-free subset of Presburger arithmetic (e.g. Detlefs et al. Simplify: a theorem prover for program checking, p. 366). --158.195.89.69 17:31, 4 July 2006 (UTC) Jan

[edit] Rewrite by anon

Some anon just rewrote most of the article, not too badly. Please check that work. Thanks. --John Nagle 05:22, 13 July 2006 (UTC)