CDCL-based abstract state transition system for coherent logic

Abstract

We present a new, CDCL-based approach for automated theorem proving in coherent logic - an expressive semi-decidable fragment of first-order logic that provides potential for obtaining human readable and machine verifiable proofs. The approach is described by means of an abstract state transition system, inspired by existing transition systems for SAT and represents its faithful lifting to coherent logic. The presented transition system includes techniques from which CDCL SAT solvers benefited the most (backjumping and lemma learning), but also allows generation of human readable proofs. In contrast to other approaches to theorem proving in coherent logic, reasoning involved need not to be ground. We prove key properties of the system, primarily that the system yields a semidecision procedure for coherent logic. As a consequence, the semidecidability of another fragment of first order logic which is a proper superset of coherent logic is also proven. © 2012 Springer-Verlag.