Nonlinear Craig Interpolant Generation over Unbounded Domains by Separating Semialgebraic Sets
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2024
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866909234933792768 |
|---|---|
| author | Wu, Hao Wang, Jie Xia, Bican Li, Xiakun Zhan, Naijun Gan, Ting |
| author_facet | Wu, Hao Wang, Jie Xia, Bican Li, Xiakun Zhan, Naijun Gan, Ting |
| contents | Interpolation-based techniques become popular in recent years, as they can improve the scalability of existing verification techniques due to their inherent modularity and local reasoning capabilities. Synthesizing Craig interpolants is the cornerstone of these techniques.
In this paper, we investigate nonlinear Craig interpolant synthesis for two polynomial formulas of the general form, essentially corresponding to the underlying mathematical problem to separate two disjoint semialgebraic sets. By combining the homogenization approach with existing techniques, we prove the existence of a novel class of non-polynomial interpolants called semialgebraic interpolants. These semialgebraic interpolants subsume polynomial interpolants as a special case. To the best of our knowledge, this is the first existence result of this kind. Furthermore, we provide complete sum-of-squares characterizations for both polynomial and semialgebraic interpolants, which can be efficiently solved as semidefinite programs. Examples are provided to demonstrate the effectiveness and efficiency of our approach. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2407_00625 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Nonlinear Craig Interpolant Generation over Unbounded Domains by Separating Semialgebraic Sets Wu, Hao Wang, Jie Xia, Bican Li, Xiakun Zhan, Naijun Gan, Ting Logic in Computer Science Interpolation-based techniques become popular in recent years, as they can improve the scalability of existing verification techniques due to their inherent modularity and local reasoning capabilities. Synthesizing Craig interpolants is the cornerstone of these techniques. In this paper, we investigate nonlinear Craig interpolant synthesis for two polynomial formulas of the general form, essentially corresponding to the underlying mathematical problem to separate two disjoint semialgebraic sets. By combining the homogenization approach with existing techniques, we prove the existence of a novel class of non-polynomial interpolants called semialgebraic interpolants. These semialgebraic interpolants subsume polynomial interpolants as a special case. To the best of our knowledge, this is the first existence result of this kind. Furthermore, we provide complete sum-of-squares characterizations for both polynomial and semialgebraic interpolants, which can be efficiently solved as semidefinite programs. Examples are provided to demonstrate the effectiveness and efficiency of our approach. |
| title | Nonlinear Craig Interpolant Generation over Unbounded Domains by Separating Semialgebraic Sets |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2407.00625 |