10 citations · 36 across the 19 of their papers we have counts for
18 papers · 1 filter
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,…
SCL(EQ): SCL for First-Order Logic with Equality
Hendrik Leidinger, Christoph Weidenbach
We propose a new calculus SCL(EQ) for first-order logic with equality that only learns non-redundant clauses. Following the idea of CDCL (Conflict Driven Clause Learning) and SCL (…
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…
SCL with Theory Constraints
Martin Bromberger, Alberto Fiori, Christoph Weidenbach
We lift the SCL calculus for first-order logic without equality to the SCL(T) calculus for first-order logic without equality modulo a background theory. In a nutshell, the SCL(T)…
The Challenge of Unifying Semantic and Syntactic Inference Restrictions
Christoph Weidenbach
While syntactic inference restrictions don't play an important role for SAT, they are an essential reasoning technique for more expressive logics, such as first-order logic, or fra…
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…
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…
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…
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…
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…
Automated Verification of Interactive Rule-Based Configuration Systems (Additional Material)
Deepak Dhungana, Ching Hoo Tang, Christoph Weidenbach +1
Additional material for the original paper "Automated Verification of Interactive Rule-Based Configuration Systems".