2 papers
cs.LO2023
First-Order Quantification over Automata
Bernard Boigelot, Pascal Fontaine, Baptiste Vergain
Deciding formulas mixing arithmetic and uninterpreted predicates is of practical interest, notably for applications in verification. Some decision procedures consist in building by…
cs.LO2023
Decidability of Difference Logic over the Reals with Uninterpreted Unary Predicates
Bernard Boigelot, Pascal Fontaine, Baptiste Vergain
First-order logic fragments mixing quantifiers, arithmetic, and uninterpreted predicates are often undecidable, as is, for instance, Presburger arithmetic extended with a single un…