6 citations · 8 across the 5 of their papers we have counts for
6 papers
Separateness of Variables -- A Novel Perspective on Decidable First-Order Fragments
Marco Voigt
The classical decision problem, as it is understood today, is the quest for a delineation between the decidable and the undecidable parts of first-order logic based on elegant synt…
On the Expressivity and Applicability of Model Representation Formalisms
Andreas Teucke, Marco Voigt, Christoph Weidenbach
A number of first-order calculi employ an explicit model representation formalism for automated reasoning and for detecting satisfiability. Many of these formalisms can represent i…
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…
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…