What's the difference between "arith" and "presburger" in Isabelle?

Question

Every goal that I have encountered in Isabelle so far that could be solved using arith could also be solved by presburger and vice versa, for example

lemma "odd (n::nat) ⟹ Suc (2 * (n div 2)) = n"
by presburger (* or arith *)

What's the difference between the two solvers? Examples of goals that one can solve but the other can't would be nice.

---

Edit: I managed to come up with a lemma proved by arith that presburger can't handle. It seems like this has something to do with real numbers:

lemma "max i (i + 1) > (i::nat)" by arith       -- ✔
lemma "max i (i + 1) > (i::nat)" by presburger  -- ✔

lemma "max i (i + 1) > (i::real)" by arith      -- ✔
lemma "max i (i + 1) > (i::real)" by presburger -- ✘

Strawser

I don't know much about either of these provers, but it would appear that presburger cannot handle real arithmetic, while arith can. I think presburger is just an implementation of the well-known decision procedure for Presburger arithmetic while arith is a collection of various decision procedures for arithmetic. There is also linarith; I do not know how that fits in. – Masera

Thanks, I hadn't even heard of linarith before (is there a comprehensive list of Isabelle/HOL methods somewhere?) – Strawser

Isn't lemma "(2 * i) div 2 = (i::real)" by presburger (which works for me) a counter-example to "presburger cannot handle real arithmetic"? – Strawser

Well I'm not entirely sure. But if you look precisely at your lemma, you will see that it needs coercions. Your statement is basically real (2 * i div 2) = real i, which is easily reduced to 2 * i div 2 = i. The reason why Isabelle inserts these coercions is that div is not defined for reals, so Isabelle defaults to int and inserts coercions to make the types work out. – Masera

Answer 1

I just asked Tobias Nipkow and this is what he told me:

• presburger is a decision procedure for Presburger arithmetic, i.e. linear arithmetic on natural numbers and integers, plus some pre-processing, which is why your statement with real could be proven as well (as it boils down to a problem on integers). It can handle quantifiers. The algorithm underlying it is known as Cooper's algorithm.
• linarith performs Fourier-Motzkin elimination to decide problems of linear arithmetic on real numbers. It can also prove these properties on natural numbers and integers, but only if they also hold on all reals. It cannot handle quantifiers.
• arith can be summarised as a combination of presburger and linarith.

For the sake of completeness, I would like to add that there are more specialised proof methods for interesting classes of statements:

• algebra uses Gröbner bases to solve goals that can be proven by rearranging terms in algebraic structures like groups and rings
• approximate computes enclosures for concrete terms using interval arithmetic
• sos can prove multivariate polynomial inequalities like (x :: real) ≥ 2 ⟹ y ≥ 2 ⟹ x + y ≤ x * y using sum-of-squares certificates
• sturm, which was written by me, can count the number of real roots in a given interval and prove certain univariate real polynomial inequalities.
• regexp can prove statements on relations like (r ∪ s⁺)* = (r ∪ s)* using regular expressions.

Masera