6 citations · 12 across the 11 of their papers we have counts for
Showing 2017Show all
3 papers · 1 filter
cs.LO2017
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…
cs.LO2017★ 1 cited
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…
cs.LO2017
Decidability of the Monadic Shallow Linear First-Order Fragment with Straight Dismatching Constraints
Andreas Teucke, Christoph Weidenbach
The monadic shallow linear Horn fragment is well-known to be decidable and has many application, e.g., in security protocol analysis, tree automata, or abstraction refinement. It w…