Decidable E*A* First-Order Fragments of Linear Rational Arithmetic with Uninterpreted Predicates

摘要

First-order linear rational arithmetic enriched with uninterpreted predicates yields an interesting and very expressive modeling language. However, already the presence of a single uninterpreted predicate symbol of arity one or greater renders the associated satisfiability problem undecidable. We identify two decidable fragments, both based on the Bernays-Schonfinkel-Ramsey prefix class. Due to the inherent infiniteness of the underlying domain, a finite model property in the usual sense cannot be established. Nevertheless, we show that satisfiable sentences always have a model that can be described by finite means. To this end, we restrict the syntax of arithmetic atoms. In the first fragment that is presented, arithmetic operations are only allowed over terms without universally quantified variables. In the second fragment, arithmetic atoms are essentially confined to difference constraints over universally quantified variables with bounded range. We will call such atomsbounded difference constraints. As bounded intervals over the rationals still comprise infinitely many values, a trivial instantiation procedure is not sufficient to solve the satisfiability problem. After a slight shift of perspective, the positive decidability result for the first fragment can be restated in the framework of combinations of theories over non-disjoint vocabularies. More precisely, we combine first-order theories that share a dense total order without endpoints.