hide
Free keywords:
Computer Science, Logic in Computer Science, cs.LO
Abstract:
We combine key ideas from first-order superposition and propositional CDCL to
create the new calculus NRCL deciding the Bernays-Sch\"onfinkel fragment. It
inherits the abstract redundancy criterion and the monotone model operator from
superposition. CDCL adds to NRCL the dynamic, conflict-driven search for an
atom ordering inducing a model. As a result, in NRCL a false clause can be
effectively found modulo the current model assumption. It guides the derivation
of a first-order ordered resolvent that is never redundant. Similar to
1UIP-learning in CDCL, the learned resolvent induces backtracking and via
propagation blocks the previous conflict state for the rest of the search.
Since learned clauses are never redundant, only finitely many can be generated
by NRCL on the Bernays-Sch\"onfinkel fragment, which provides a nice argument
for termination.
