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.

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

19 Documents citing this article

Dennis Peuter;Viorica Sofronie-Stokkermans;Sebastian Thunert, Lecture notes in computer science, 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}^+$$, pp. 419-437, 2023, 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, https://doi.org/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, Lecture notes in computer science, Interpolation and Amalgamation for Arrays with MaxDiff, pp. 268-288, 2021, 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, Lecture notes in computer science, Nonlinear Craig Interpolant Generation, pp. 415-438, 2020, 10.1007/978-3-030-53288-8_20, https://doi.org/10.1007/978-3-030-53288-8_20.

Dennis Peuter;Viorica Sofronie-Stokkermans, arXiv (Cornell University), On Invariant Synthesis for Parametric Systems, pp. 385-405, 2019, 10.1007/978-3-030-29436-6_23, https://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, https://doi.org/10.1145/3093333.3009864.

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

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

Nishant Totla;Thomas Wies, 2016, Complete Instantiation-Based Interpolation, CiteSeer X (The Pennsylvania State University), 57, 1, pp. 37-65, 10.1007/s10817-016-9371-7, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.650.7623.

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

Viorica Sofronie-Stokkermans, arXiv (Cornell University), On Interpolation and Symbol Elimination in Theory Extensions, pp. 273-289, 2016, 10.1007/978-3-319-40229-1_19, http://arxiv.org/abs/1702.06620.

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, arXiv (Cornell University), On First-Order Model-Based Reasoning, pp. 181-204, 2015, 10.1007/978-3-319-23165-5_8, https://arxiv.org/abs/1502.02535.

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

Nishant Totla;Thomas Wies, 2013, Complete instantiation-based interpolation, CiteSeer X (The Pennsylvania State University), 48, 1, pp. 537-548, 10.1145/2480359.2429132, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.295.8370.

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, https://doi.org/10.1016/j.jsc.2010.06.005.

Sources : OpenCitations, OpenAlex & Crossref

Share and export

Consultation statistics

This page has been seen 1699 times.

This article's PDF has been downloaded 489 times.