Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2506.01664 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866909632747798528 |
|---|---|
| author | Sofronie-Stokkermans, Viorica |
| author_facet | Sofronie-Stokkermans, Viorica |
| contents | We define a notion of general uniform interpolant, generalizing the notions of cover and of uniform interpolant and identify situations in which symbol elimination can be used for computing general uniform interpolants. We investigate the limitations of the method we propose, and identify theory extensions for which the computation of general uniform interpolants can be reduced to symbol elimination followed by the computation of uniform quantifier-free interpolants in extensions with uninterpreted function symbols of theories allowing uniform quantifier-free interpolation. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2506_01664 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | On Symbol Elimination and Uniform Interpolation in Theory Extensions Sofronie-Stokkermans, Viorica Logic in Computer Science We define a notion of general uniform interpolant, generalizing the notions of cover and of uniform interpolant and identify situations in which symbol elimination can be used for computing general uniform interpolants. We investigate the limitations of the method we propose, and identify theory extensions for which the computation of general uniform interpolants can be reduced to symbol elimination followed by the computation of uniform quantifier-free interpolants in extensions with uninterpreted function symbols of theories allowing uniform quantifier-free interpolation. |
| title | On Symbol Elimination and Uniform Interpolation in Theory Extensions |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2506.01664 |