What's the difference between "arith" and "presburger" in Isabelle?
isabelle, solver, theorem-proving
Solution
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.
Problem
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 -- ✘ ```