Constraint Learning for Non-confluent Proof Search
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2026
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866911489117388800 |
|---|---|
| author | Rawson, Michael Eisenhofer, Clemens Kovács, Laura |
| author_facet | Rawson, Michael Eisenhofer, Clemens Kovács, Laura |
| contents | Proof search in non-confluent tableau calculi, such as the connection tableau calculus, suffers from excess backtracking, but simple restrictions on backtracking are incomplete. We adopt constraint learning to reduce backtracking in the classical first-order connection calculus, while retaining completeness. An initial constraint learning language for connection-driven search is iteratively refined to greatly reduce backtracking in practice. The approach may be useful for proof search in other non-confluent tableau calculi. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2603_05258 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Constraint Learning for Non-confluent Proof Search Rawson, Michael Eisenhofer, Clemens Kovács, Laura Logic in Computer Science Proof search in non-confluent tableau calculi, such as the connection tableau calculus, suffers from excess backtracking, but simple restrictions on backtracking are incomplete. We adopt constraint learning to reduce backtracking in the classical first-order connection calculus, while retaining completeness. An initial constraint learning language for connection-driven search is iteratively refined to greatly reduce backtracking in practice. The approach may be useful for proof search in other non-confluent tableau calculi. |
| title | Constraint Learning for Non-confluent Proof Search |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2603.05258 |