Finding Connections via Satisfiability Solving
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , |
|---|---|
| Format: | Preprint |
| Publié: |
2026
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866910043727724544 |
|---|---|
| author | Eisenhofer, Clemens Rawson, Michael Kovács, Laura |
| author_facet | Eisenhofer, Clemens Rawson, Michael Kovács, Laura |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2603_06345 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Finding Connections via Satisfiability Solving Eisenhofer, Clemens Rawson, Michael Kovács, Laura Logic in Computer Science 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. |
| title | Finding Connections via Satisfiability Solving |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2603.06345 |