Interpolation in local theory extensions

Viorica Sofronie-Stokkermans

doi:10.2168/LMCS-4(4:1)2008

Viorica Sofronie-Stokkermans - Interpolation in local theory extensions

lmcs:1143 - Logical Methods in Computer Science, October 17, 2008, Volume 4, Issue 4 - https://doi.org/10.2168/LMCS-4(4:1)2008

Interpolation in local theory extensionsArticle

Authors: Viorica Sofronie-Stokkermans

In this paper we study interpolation in local extensions of a base theory. We identify situations in which it is possible to obtain interpolants in a hierarchical manner, by using a prover and a procedure for generating interpolants in the base theory as black-boxes. We present several examples of theory extensions in which interpolants can be computed this way, and discuss applications in verification, knowledge representation, and modular reasoning in combinations of local theories.

Comment: 31 pages, 1 figure

https://doi.org/10.2168/LMCS-4(4:1)2008

Source: arXiv.org:0806.4553

Volume: Volume 4, Issue 4

Published on: October 17, 2008

Imported on: February 11, 2007

Keywords: Computer Science - Logic in Computer Science, Computer Science - Software Engineering, F.4.1, F.3.1

Licence: arXiv.org - Non-exclusive license to distribute

Classifications

Mathematics Subject Classification 2020¹

68N18 - Functional programming and lambda calculus

Sources:

[1] zbMATH Open.

Bibliographic References

20 Documents citing this article

Hao Wu;Jie Wang;Bican Xia;Xiakun Li;Naijun Zhan;et al., 2024, Nonlinear Craig Interpolant Generation Over Unbounded Domains by Separating Semialgebraic Sets, Lecture notes in computer science, pp. 92-110, 10.1007/978-3-031-71162-6_5, https://doi.org/10.1007/978-3-031-71162-6_5.

Dennis Peuter;Viorica Sofronie-Stokkermans;Sebastian Thunert, 2023, On P-Interpolation in Local Theory Extensions and Applications to the Study of Interpolation in the Description Logics $$\mathcal{E}\mathcal{L}, \mathcal{E}\mathcal{L}^+$$, Lecture notes in computer science, pp. 419-437, 10.1007/978-3-031-38499-8_24, https://doi.org/10.1007/978-3-031-38499-8_24.

Silvio Ghilardi;Alessandro Gianola;Deepak Kapur;Chiara Naso, 2023, Interpolation Results for Arrays with Length and MaxDiff, ACM Transactions on Computational Logic, 24, 4, pp. 1-33, 10.1145/3587161.

Silvio Ghilardi;Alessandro Gianola, 2022, Interpolation and Uniform Interpolation in Quantifier-Free Fragments of Combined First-Order Theories, Mathematics, 10, 3, pp. 461, 10.3390/math10030461, https://doi.org/10.3390/math10030461.

Silvio Ghilardi;Alessandro Gianola;Deepak Kapur, 2021, Interpolation and Amalgamation for Arrays with MaxDiff, Lecture notes in computer science, pp. 268-288, 10.1007/978-3-030-71995-1_14, https://doi.org/10.1007/978-3-030-71995-1_14.

Diego Calvanese;Silvio Ghilardi;Alessandro Gianola;Marco Montali;Andrey Rivkin, 2020, SMT-based verification of data-aware processes: a model-theoretic approach, Archivio Istituzionale della Ricerca (Universita Degli Studi Di Milano), 30, 3, pp. 271-313, 10.1017/s0960129520000067, http://hdl.handle.net/2434/730867.

Ting Gan;Bican Xia;Bai Xue;Naijun Zhan;Liyun Dai, 2020, Nonlinear Craig Interpolant Generation, Lecture notes in computer science, pp. 415-438, 10.1007/978-3-030-53288-8_20, https://doi.org/10.1007/978-3-030-53288-8_20.

Dennis Peuter;Viorica Sofronie-Stokkermans, 2019, On Invariant Synthesis for Parametric Systems, arXiv (Cornell University), pp. 385-405, 10.1007/978-3-030-29436-6_23, http://arxiv.org/abs/1905.12524.

Silvio Ghilardi;Alessandro Gianola, 2018, Modularity results for interpolation, amalgamation and superamalgamation, Archivio Istituzionale della Ricerca (Universita Degli Studi Di Milano), 169, 8, pp. 731-754, 10.1016/j.apal.2018.04.001, http://hdl.handle.net/2434/570431.

Akhilesh Srikanth;Burak Sahin;William R. Harris, 2017, Complexity verification using guided theorem enumeration, ACM SIGPLAN Notices, 52, 1, pp. 639-652, 10.1145/3093333.3009864.

Silvio Ghilardi;Alessandro Gianola, 2017, Interpolation, Amalgamation and Combination (The Non-disjoint Signatures Case), Lecture notes in computer science, pp. 316-332, 10.1007/978-3-319-66167-4_18.

Akhilesh Srikanth;Burak Sahin;William R. Harris, 2016, Complexity verification using guided theorem enumeration, Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, pp. 639-652, 10.1145/3009837.3009864.

Nishant Totla;Thomas Wies, 2016, Complete Instantiation-Based Interpolation, Journal of Automated Reasoning, 57, 1, pp. 37-65, 10.1007/s10817-016-9371-7.

Ting Gan;Liyun Dai;Bican Xia;Naijun Zhan;Deepak Kapur;et al., 2016, Interpolant Synthesis for Quadratic Polynomial Inequalities and Combination with EUF, Lecture notes in computer science, pp. 195-212, 10.1007/978-3-319-40229-1_14.

Viorica Sofronie-Stokkermans, 2016, On Interpolation and Symbol Elimination in Theory Extensions, Lecture notes in computer science, pp. 273-289, 10.1007/978-3-319-40229-1_19.

Maria Paola Bonacina;Moa Johansson, 2015, Interpolation Systems for Ground Proofs in Automated Deduction: a Survey, Journal of Automated Reasoning, 54, 4, pp. 353-390, 10.1007/s10817-015-9325-5.

Maria Paola Bonacina;Ulrich Furbach;Viorica Sofronie-Stokkermans;Maria Paola Bonacina;Ulrich Furbach;et al., 2015, On First-Order Model-Based Reasoning, arXiv (Cornell University), pp. 181-204, 10.1007/978-3-319-23165-5_8, http://arxiv.org/abs/1502.02535.

Wei Wang;Clark Barrett;Thomas Wies, 2014, Cascade 2.0, Lecture notes in computer science, pp. 142-160, 10.1007/978-3-642-54013-4_9.

Nishant Totla;Thomas Wies, 2013, Complete instantiation-based interpolation, ACM SIGPLAN Notices, 48, 1, pp. 537-548, 10.1145/2480359.2429132.

Andrey Rybalchenko;Viorica Sofronie-Stokkermans, 2010, Constraint solving for interpolation, Journal of Symbolic Computation, 45, 11, pp. 1212-1233, 10.1016/j.jsc.2010.06.005.

Sources : OpenCitations, OpenAlex & Crossref

Share and export

Consultation statistics

This page has been seen 3060 times.

This article's PDF has been downloaded 614 times.