Timeline for Effortless automated proofs for "simple" formulae?
Current License: CC BY-SA 4.0
5 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| May 28 at 8:25 | comment | added | Jérôme JEAN-CHARLES | @Emil Jeřábek : Very clear, thank you. | |
| May 27 at 21:28 | comment | added | Emil Jeřábek | $\min$ and $\max$ are quantifier-free definable from order: e.g., $\min(x,y)=z\iff(x\le y\land z=x)\lor(y\le x\land z=y)$. The bounds are explicit, and the exponent should be something small (2 or 3 or so), but I can’t search the literature now. | |
| May 27 at 20:14 | comment | added | Jérôme JEAN-CHARLES | @Emil Jeřábek : Taking a quick look at Pressburger Arith : Is the degree of polynomial constructive, and I am not sure how to cover Min(i,j) or Max() ? | |
| May 27 at 13:56 | comment | added | Emil Jeřábek | You seem to be asking about the size of a minimal counterexample to a universal sentence of Presburger arithmetic, or equivalently, of a minimal solution of an integer linear program. These are known to have bit-length polynomial in the length of the formula. | |
| May 27 at 13:29 | history | asked | Jérôme JEAN-CHARLES | CC BY-SA 4.0 |