7 citations · 19 across the 8 of their papers we have counts for
5 papers · 1 filter
The Bernays-Schönfinkel-Ramsey Fragment with Bounded Difference Constraints over the Reals is Decidable
Marco Voigt
First-order linear real arithmetic enriched with uninterpreted predicate symbols yields an interesting modeling language. However, satisfiability of such formulas is undecidable, e…
On Generalizing Decidable Standard Prefix Classes of First-Order Logic
Marco Voigt
Recently, the separated fragment (SF) of first-order logic has been introduced. Its defining principle is that universally and existentially quantified variables may not occur toge…
On the Combination of the Bernays-Schönfinkel-Ramsey Fragment with Simple Linear Integer Arithmetic
Matthias Horbach, Marco Voigt, Christoph Weidenbach
In general, first-order predicate logic extended with linear integer arithmetic is undecidable. We show that the Bernays-Schönfinkel-Ramsey fragment (-sentence…
A Fine-Grained Hierarchy of Hard Problems in the Separated Fragment
Marco Voigt
Recently, the separated fragment (SF) has been introduced and proved to be decidable. Its defining principle is that universally and existentially quantified variables may not occu…
The Universal Fragment of Presburger Arithmetic with Unary Uninterpreted Predicates is Undecidable
Matthias Horbach, Marco Voigt, Christoph Weidenbach
The first-order theory of addition over the natural numbers, known as Presburger arithmetic, is decidable in double exponential time. Adding an uninterpreted unary predicate to the…