Finding Connections via Satisfiability Solving
This work addresses the challenge of improving automation in first-order logic proof search for automated reasoners, though it appears incremental as it builds on existing approaches.
The paper tackles the problem of automating first-order classical logic proofs by combining ordering-based saturation and goal reduction into a SAT-based method with symmetry breaking for connection calculi, resulting in the implementation of a new solver called upCoP that demonstrates practical feasibility.
Commonly used proof strategies by automated reasoners organise proof search either by ordering-based saturation or by reducing goals to subgoals. In this paper, we combine these two approaches and advocate a SAT-based method with symmetry breaking for connection calculi in first-order logic, with the purpose of further pushing the automation in first-order classical logic proofs. In contrast to classical ways of reducing first-order logic to propositional logic, our method encodes the structure of the proof search itself. We present three distinct SAT encodings for connection calculi, analyse their theoretical properties, and discuss the effect of using SAT/SMT solvers on these encodings. We implemented our work in the new solver upCoP and showcase its practical feasibility.