SCL(FOL) Revisited
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2023
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866929281715666944 |
|---|---|
| author | Bromberger, Martin Schwarz, Simon Weidenbach, Christoph |
| author_facet | Bromberger, Martin Schwarz, Simon Weidenbach, Christoph |
| contents | This paper presents an up-to-date and refined version of the SCL calculus for first-order logic without equality. The refinement mainly consists of the following two parts: First, we incorporate a stronger notion of regularity into SCL(FOL). Our regularity definition is adapted from the SCL(T) calculus. This adapted definition guarantees non-redundant clause learning during a run of SCL. However, in contrast to the original presentation, it does not require exhaustive propagation. Second, we introduce trail and model bounding to achieve termination guarantees. In previous versions, no termination guarantees about SCL were achieved. Last, we give rigorous proofs for soundness, completeness and clause learning guarantees of SCL(FOL) and put SCL(FOL) into context of existing first-order calculi. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2302_05954 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | SCL(FOL) Revisited Bromberger, Martin Schwarz, Simon Weidenbach, Christoph Logic in Computer Science Symbolic Computation This paper presents an up-to-date and refined version of the SCL calculus for first-order logic without equality. The refinement mainly consists of the following two parts: First, we incorporate a stronger notion of regularity into SCL(FOL). Our regularity definition is adapted from the SCL(T) calculus. This adapted definition guarantees non-redundant clause learning during a run of SCL. However, in contrast to the original presentation, it does not require exhaustive propagation. Second, we introduce trail and model bounding to achieve termination guarantees. In previous versions, no termination guarantees about SCL were achieved. Last, we give rigorous proofs for soundness, completeness and clause learning guarantees of SCL(FOL) and put SCL(FOL) into context of existing first-order calculi. |
| title | SCL(FOL) Revisited |
| topic | Logic in Computer Science Symbolic Computation |
| url | https://arxiv.org/abs/2302.05954 |