Showing cs.LOShow all
2 papers · 1 filter
cs.LO2026
Fast Ramsey Quantifier Elimination in LIRA (with applications to liveness checking)
Kilian Lichtner, Pascal BergsträÃer, Moses Ganardi +2
Ramsey quantifiers have recently been proposed as a unified framework for handling properties of interests in program verification involving proofs in the form of infinite cliques,…
cs.LO2024
An efficient quantifier elimination procedure for Presburger arithmetic
Christoph Haase, Shankara Narayanan Krishna, Khushraj Madnani +2
All known quantifier elimination procedures for Presburger arithmetic require doubly exponential time for eliminating a single block of existentially quantified variables. It has e…