Interpolation in local theory extensions. (English) Zbl 1222.03018
Furbach, Ulrich (ed.) et al., Automated reasoning. Third international joint conference, IJCAR 2006, Seattle, WA, USA, August 17–20, 2006. Proceedings. Berlin: Springer (ISBN 978-3-540-37187-8/pbk). Lecture Notes in Computer Science 4130. Lecture Notes in Artificial Intelligence, 235-250 (2006).
Summary: 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.
For the entire collection see [Zbl 1120.68005].
For the entire collection see [Zbl 1120.68005].
MSC:
| 03B35 | Mechanization of proofs and logical operations |
