Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Finding Connections via Satisfiability Solving

Clemens Eisenhofer, Michael Rawson, Laura Kovács

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.

Finding Connections via Satisfiability Solving

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.
Paper Structure (30 sections, 10 theorems, 22 equations, 3 figures)

This paper contains 30 sections, 10 theorems, 22 equations, 3 figures.

Table of Contents

  1. Introduction
  2. Summary of Contributions.
  3. Preliminaries
  4. Satisfiability Solving
  5. Connection Tableaux
  6. The Connection Method, Matrices, and Spanning Connections
  7. Encoding Connection Tableaux
  8. Connection tableau rules as SAT.
  9. Unification Constraints.
  10. SAT Encoding of Closed Connection Tableaux.
  11. Pathological Behaviour.
  12. Encoding Matrix Proofs
  13. Encoding Overview
  14. Fully Connected Matrices
  15. Spanning Sets of Connections
  16. ...and 15 more sections

Key Result

theorem 1

Suppose $M$ is a minimal matrix proof with a spanning set of connections. Then $M$ is fully connected.

Figures (3)

  • Figure 1: Connection tableau rules, left-to-right: start, extension, and reduction. In start and extension, $L \vee \ldots \vee K$ is a freshly-renamed copy of a clause from the input problem. In extension and reduction, $L$ is connected to $L'$ using $\sigma$.
  • Figure 2: Connection calculus derivations
  • Figure 3: Experimental summary. UPCoP$_{{\tt SAT}}$ and UPCoP$_{{\tt SMT}}$ denote the UPCoP versions based on CaDiCaL (SAT) and Z3 (SMT). "Unique" lists the number of problems solvable by UPCoP, but not meanCoP, and vice versa.

Theorems & Definitions (17)

  • theorem 1: Fully Connected Matrix
  • proof
  • theorem 2: Soundness
  • proof
  • theorem 3: Completeness
  • proof
  • theorem 4: Complexity Bound
  • proof
  • corollary 1: Termination
  • theorem 5: Completeness
  • ...and 7 more