7 citations · 19 across the 8 of their papers we have counts for
9 papers · 1 filter
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…
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…
Deciding First-Order Satisfiability when Universal and Existential Variables are Separated
Thomas Sturm, Marco Voigt, Christoph Weidenbach
We introduce a new decidable fragment of first-order logic with equality, which strictly generalizes two already well-known ones -- the Bernays-Schönfinkel-Ramsey (BSR) Fragment an…
Bernays-Schoenfinkel-Ramsey with Simple Bounds is NEXPTIME-complete
Marco Voigt, Christoph Weidenbach
First-order predicate logic extended with linear arithmetic is undecidable, in general. We show that the Bernays-Schönfinkel-Ramsey (BSR) fragment extended with linear arithmetic r…