Finding Connections via Satisfiability Solving

TL;DR

This paper introduces a SAT-based method with symmetry breaking for connection calculi in first-order logic, aiming to enhance automation in classical logic proofs by encoding proof search structures.

Contribution

It combines ordering-based saturation and goal reduction approaches, presenting three SAT encodings and analyzing their properties for improved proof automation.

Findings

Developed three SAT encodings for connection calculi

Analyzed theoretical properties of the encodings

Implemented in the new solver upCoP demonstrating practical feasibility

Abstract

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.