When Less Is More: Consequence-Finding in a Weak Theory of Arithmetic
summary
Presents a decidable first‑order theory called LIRR (linear integer/real with weak multiplication), a concrete axiomatization and an effective model construction based on algebraic cones that are finitely generated and closed under projection, intersection and homomorphism. Implements an algorithm that computes the strongest conjunctive consequences of a ground formula and a monotone invariant generation scheme extracting linear/nonlinear summaries and recurrences. Experiments show the solver is not competitive on general satisfiability tasks but yields useful non‑linear invariants on program benchmarks, outperforming prior tools in the non‑linear category after heuristics.
AI-written summary · about
chapters (15)
- 0:00Consequence finding in arithmetic
- 1:59Program analysis applications
- 3:01Introducing LIRR theory
- 4:06LIRR model structure
- 6:55LIRR axioms for integers
- 8:21LIRR decidability and expressiveness
- 9:43Algebraic cones in model theory
- 11:49Satisfiability in LIRR
- 13:13Algebraic cones and models
- 14:58Effective consequence computation
- 16:43Stronger consequence finding
- 18:06Consequence cones for invariants
- 19:10Monotone invariant generation
- 20:15Program verification results
- 21:50Q&A
related talks
19mRamsey Quantifiers in Linear Arithmetics
01h 02mAlgebraic Structures in Logic and Query Evaluation 3
01h 08mAlgebraic Structures in Logic and Query Evaluation 4
28mThe Logic of Counting Query Answers
20mThe Decision Problem for Regular First Order Theories
01h 24mIntroduction to Constraint Logic Programming
41mOptimizing Relational Programs I
36mOptimizing Relational Programs II