Superposition with Delayed Unification
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866910358208249856 |
|---|---|
| author | Bhayat, Ahmed Schoisswohl, Johannes Rawson, Michael |
| author_facet | Bhayat, Ahmed Schoisswohl, Johannes Rawson, Michael |
| contents | Classically, in saturation-based proof systems, unification has been considered atomic. However, it is also possible to move unification to the calculus level, turning the steps of the unification algorithm into inferences. For calculi that rely on unification procedures returning large or even infinite sets of unifiers, integrating unification into the calculus is an attractive method of dovetailing unification and inference. This applies, for example, to AC-superposition and higher-order superposition. We show that first-order superposition remains complete when moving unification rules to the calculus level. We discuss some of the benefits this has even for standard first-order superposition and provide an experimental evaluation. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2403_04775 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Superposition with Delayed Unification Bhayat, Ahmed Schoisswohl, Johannes Rawson, Michael Logic in Computer Science Artificial Intelligence Classically, in saturation-based proof systems, unification has been considered atomic. However, it is also possible to move unification to the calculus level, turning the steps of the unification algorithm into inferences. For calculi that rely on unification procedures returning large or even infinite sets of unifiers, integrating unification into the calculus is an attractive method of dovetailing unification and inference. This applies, for example, to AC-superposition and higher-order superposition. We show that first-order superposition remains complete when moving unification rules to the calculus level. We discuss some of the benefits this has even for standard first-order superposition and provide an experimental evaluation. |
| title | Superposition with Delayed Unification |
| topic | Logic in Computer Science Artificial Intelligence |
| url | https://arxiv.org/abs/2403.04775 |