Decidable $\exists$*$\forall$* First-Order Fragments of Linear Rational Arithmetic with Uninterpreted Predicates - Archive ouverte HAL Access content directly
Journal Articles Journal of Automated Reasoning Year : 2021

## Decidable $\exists$*$\forall$* First-Order Fragments of Linear Rational Arithmetic with Uninterpreted Predicates

Marco Voigt

#### Abstract

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– Schönfinkel–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 termswithout 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 atoms bounded 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.

#### Domains

Computer Science [cs]

### Dates and versions

hal-03531894 , version 1 (18-01-2022)

### Identifiers

• HAL Id : hal-03531894 , version 1
• DOI :

### Cite

Marco Voigt. Decidable $\exists$*$\forall$* First-Order Fragments of Linear Rational Arithmetic with Uninterpreted Predicates. Journal of Automated Reasoning, 2021, 65 (3), pp.357-423. ⟨10.1007/s10817-020-09567-8⟩. ⟨hal-03531894⟩

### Export

BibTeX TEI Dublin Core DC Terms EndNote Datacite

20 View