Computing Witnesses Using the SCAN Algorithm (Extended Preprint)
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866910977759379456 |
|---|---|
| author | Achammer, Fabian Hetzl, Stefan Schmidt, Renate A. |
| author_facet | Achammer, Fabian Hetzl, Stefan Schmidt, Renate A. |
| contents | Second-order quantifier-elimination is the problem of finding, given a formula with second-order quantifiers, a logically equivalent first-order formula. While such formulas are not computable in general, there are practical algorithms and subclasses with applications throughout computational logic. One of the most prominent algorithms for second-order quantifier elimination is the SCAN algorithm which is based on saturation theorem proving. In this paper we show how the SCAN algorithm on clause sets can be extended to solve a more general problem: namely, finding an instance of the second-order quantifiers that results in a logically equivalent first-order formula. In addition we provide a prototype implementation of the proposed method. This work paves the way for applying the SCAN algorithm to new problems in application domains such as modal correspondence theory, knowledge representation, and verification. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2506_00163 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Computing Witnesses Using the SCAN Algorithm (Extended Preprint) Achammer, Fabian Hetzl, Stefan Schmidt, Renate A. Logic in Computer Science Second-order quantifier-elimination is the problem of finding, given a formula with second-order quantifiers, a logically equivalent first-order formula. While such formulas are not computable in general, there are practical algorithms and subclasses with applications throughout computational logic. One of the most prominent algorithms for second-order quantifier elimination is the SCAN algorithm which is based on saturation theorem proving. In this paper we show how the SCAN algorithm on clause sets can be extended to solve a more general problem: namely, finding an instance of the second-order quantifiers that results in a logically equivalent first-order formula. In addition we provide a prototype implementation of the proposed method. This work paves the way for applying the SCAN algorithm to new problems in application domains such as modal correspondence theory, knowledge representation, and verification. |
| title | Computing Witnesses Using the SCAN Algorithm (Extended Preprint) |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2506.00163 |