7 citations · 19 across the 8 of their papers we have counts for
Showing 2015Show all
2 papers · 1 filter
cs.LO2015★ 7 cited
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…
cs.LO2015★ 4 cited
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…