Talk:Presburger arithmetic

From Wikipedia, the free encyclopedia

WikiProject Mathematics
Mathematics Portal
This article is within the scope of WikiProject Mathematics, which collaborates on articles related to mathematics.
Mathematics rating: Start Class Low Priority  Field: Foundations, logic, and set theory
Please update this rating as the article progresses, or if the rating is inaccurate. Please also add comments to suggest improvements to the article.

Contents

[edit] Early comments

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)


[edit] simplex

I do not understand why simplex has anything to do with Presburger. Presburger is for natural numbers, whereas simplex is for the reals. Simplex might be used inside an algorithm such as branch & bound to solve the ILP part, but this is not what is written in the page.

[edit] induction

Shouldn't there be some explicit mention of quantifiers in the induction axiom?

(P(0) AND (P(x)->P(x+1))->P(x)

say P is "is even." Now P(0)->P(1) is false so the axiom is vacuously true for x=0. P(0) AND P(1)->P(2) is true, but P(1) is false, hence the axiom fails. I think one wants two variables. Thoughts? MotherFunctor (talk) 17:17, 27 November 2007 (UTC)

Yes, the third x should be a y or some other variable. — Carl (CBM · talk) 17:47, 27 November 2007 (UTC)

[edit] Decision using automata etc.

We should discuss the various decision procedures:

  • Omega
  • Wolper et al.'s methods using finite automata (for instance, the LIRA tool). David.Monniaux (talk) 07:24, 10 December 2007 (UTC)

[edit] Language

I removed phrases like 'invokes an object constant' in favor of what I feel to be more standard expressions; also -- equality: is it a nonlogical constant, therefore a predicate of the language of Presburger arithmetic (as the original revision had it) OR is the background logic 'first order logic with identity' in which case equality is NOT just another predicate. I favor the latter. Zero sharp (talk) 21:16, 7 April 2008 (UTC)

[edit] moved from article

"The Wikipedia reference is slightly incorrect. The upper bound grows exponentially by the size of the problem, so is infinitely large, not bounded as suggested by Wikipedia. It is, Oppen believes, the largest bounded problem thus shown" added by user User:Derekoppen Zero sharp (talk) 06:27, 1 June 2008 (UTC)


[edit] self-reference

Could someone advise on the propriety of one putting references to one's own work in a WP article (Derek C. Oppen as user 'Derekoppen' added a reference to one of his own journal articles). Thanks. Zero sharp (talk) 18:30, 2 June 2008 (UTC)

See WP:COS and WP:COI. One should be cautious with such edits, but ultimately the standard is the same as if anybody else inserted the reference: if it's relevant, notable, and properly sourced, it's OK. In this particular case[1], I think the edit was entirely appropriate, except that it was somewhat misplaced (that's why I moved it and slightly reformulated). Notice also that the reference to Oppen and Nelson (1980) was added by someone else. — EJ (talk) 10:02, 3 June 2008 (UTC)
Understood, thanks very much. Zero sharp (talk) 14:52, 3 June 2008 (UTC)