Ramsey Quantifiers in Linear Arithmetics
summary
Proves an elimination procedure for Ramsey quantifiers over Linear Integer, Real, and mixed arithmetic (LIA, LRA, LIRA) that, for existential input formulas, constructs an equivalent existential formula in polynomial time and of linear size, enabling off‑the‑shelf SMT solvers to check well‑foundedness and infinite cliques. Derives NP/coNP complexity bounds for termination, liveness and monadic decomposability (monadic decomposability shown coNP‑complete), gives a prototype implementation with encouraging micro‑benchmark results, and describes the matrix/profile construction used.
AI-written summary · about
chapters (10)
- 0:00Ramsey quantifiers in linear arithmetic
- 1:06Termination analysis of real-integer program
- 3:14Non-terminating convergent behavior
- 4:40Ramsey quantifier for infinite paths
- 7:13Eliminating Ramsey quantifiers for SMT
- 8:18Polynomial-time elimination result
- 11:08Click existence proof strategy
- 13:58Applications to linear liveness and NP-completeness
- 15:20Quasi-order and decomposability results
- 16:42Q&A
related talks
24mWhen Less Is More: Consequence-Finding in a Weak Theory of Arithmetic
01h 08mAlgebraic Structures in Logic and Query Evaluation 4
01h 05mAlgebraic Structures in Logic and Query Evaluation 2
28mThe Logic of Counting Query Answers
35mApproximating Certain and Possible Answers Beyond Sets
36mOptimizing Relational Programs II
21mGenerating Collection Transformations from Proofs
01h 03mQuery Optimization and Evaluation 3: Variable Elimination and Tensor Decomposition