Tags:Bernays-Schoenfinkel Fragment, Clause Learning, Decision Procedure and Explicit Model Representation
Abstract:
Several decision procedures for the Bernays-Schoenfinkel fragment of first-order logic rely on explicit model assumptions. In particular, the procedures differ in their respective model representation formalisms. We introduce a new decision procedure SCL for clause learning from simple models. Simple models are solely build on ground literals. Nevertheless, we show that SCL can learn exactly the clauses other procedures learn with respect to more complex model representation formalisms. Therefore, the overhead of complex model representation formalisms is not always needed.