10 citations · 19 across the 8 of their papers we have counts for
3 papers · 1 filter
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,…