10 citations · 19 across the 8 of their papers we have counts for
8 papers
A Two-Watched Literal Scheme for First-Order Logic
Yasmine Briefs, Martin Bromberger, Tobias Gehl +3
The two-watched literal scheme, a core component of efficient CDCL (Conflict-Driven Clause Learning) implementations for propositional logic, is extended to first-order logic. Give…
SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning
Martin Bromberger, Chaahat Jain, Christoph Weidenbach
We show that SCL(FOL) can simulate the derivation of non-redundant clauses by superposition for first-order logic without equality. Superposition-based reasoning is performed with…
Symbolic Model Construction for Saturated Constrained Horn Clauses
Martin Bromberger, Lorenz Leutgeb, Christoph Weidenbach
Clause sets saturated by hierarchic ordered resolution do not offer a model representation that can be effectively queried, in general. They only offer the guarantee of the existen…
SCL(FOL) Revisited
Martin Bromberger, Simon Schwarz, Christoph Weidenbach
This paper presents an up-to-date and refined version of the SCL calculus for first-order logic without equality. The refinement mainly consists of the following two parts: First,…
A Sorted Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic
Martin Bromberger, Irina Dragoste, Rasha Faqeh +6
In a previous paper, we have shown that clause sets belonging to the Horn Bernays-Schönfinkel fragment over simple linear real arithmetic (HBS(SLR)) can be translated into HBS clau…
A Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic
Martin Bromberger, Irina Dragoste, Rasha Faqeh +3
The Bernays-Schönfinkel first-order logic fragment over simple linear real arithmetic constraints BS(SLR) is known to be decidable. We prove that BS(SLR) clause sets with both univ…
A Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded Problems
Martin Bromberger
We present a combination of the Mixed-Echelon-Hermite transformation and the Double-Bounded Reduction for systems of linear mixed arithmetic that preserve satisfiability and can be…
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…