10 citations · 36 across the 19 of their papers we have counts for
5 papers · 1 filter
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…
First-Order Logic Theorem Proving and Model Building via Approximation and Instantiation
Andreas Teucke, Christoph Weidenbach
In this paper we consider first-order logic theorem proving and model building via approximation and instantiation. Given a clause set we propose its approximation into a simplifie…
Linear Integer Arithmetic Revisited
Martin Bromberger, Thomas Sturm, Christoph Weidenbach
We consider feasibility of linear integer programs in the context of verification systems such as SMT solvers or theorem provers. Although satisfiability of linear integer programs…
NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment (Full Paper)
Gábor Alagi, Christoph Weidenbach
We combine constrained literals for model representation with key concepts from first-order superposition and propositional conflict-driven clause learning (CDCL) to create the new…
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…