2 citations · 5 across the 7 of their papers we have counts for
9 papers
Connection-minimal Abduction in EL via Translation to FOL -- Technical Report
Fajar Haifani, Patrick Koopmann, Sophie Tourret +1
Abduction in description logics finds extensions of a knowledge base to make it entail an observation. As such, it can be used to explain why the observation does not follow, to re…
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…