Decidability of Difference Logic over the Reals with Uninterpreted Unary Predicates
Abstract
First-order logic fragments mixing quantifiers, arithmetic, and uninterpreted predicates are often undecidable, as is, for instance, Presburger arithmetic extended with a single uninterpreted unary predicate. In the SMT world, difference logic is a quite popular fragment of linear arithmetic which is less expressive than Presburger arithmetic. Difference logic on integers with uninterpreted unary predicates is known to be decidable, even in the presence of quantifiers. We here show that (quantified) difference logic on real numbers with a single uninterpreted unary predicate is undecidable, quite surprisingly. Moreover, we prove that difference logic on integers, together with order on reals, combined with uninterpreted unary predicates, remains decidable.
Keywords
Cite
@article{arxiv.2305.15059,
title = {Decidability of Difference Logic over the Reals with Uninterpreted Unary Predicates},
author = {Bernard Boigelot and Pascal Fontaine and Baptiste Vergain},
journal= {arXiv preprint arXiv:2305.15059},
year = {2023}
}
Comments
This is the preprint for the submission published in CADE-29. It also includes an additional detailed proof in the appendix. The Version of Record of this contribution will be published in CADE-29