INTERPOLATION IN LOCAL THEORY EXTENSIONS

被引：13
作者：
Sofronie-Stokkermans, Viorica [1 ]
机构：
[1] Max Planck Inst Informat, Saarbrucken, Germany
来源：
LOGICAL METHODS IN COMPUTER SCIENCE | 2008年 / 4卷 / 04期
关键词：
Logic; Interpolation; Complex theories; Verification; Knowledge representation;
D O I：
10.2168/LMCS-4(4:1)2008
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
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.
引用
收藏
页数：31
相关论文
共 19 条
[1]  
Baader F, 2005, LECT NOTES ARTIF INT, V3632, P278
[2]  
Bacsich Paul D., 1975, Algebra Universalis, V5, P45
[3]  
Cimatti A, 2008, LECT NOTES COMPUT SC, V4963, P397, DOI 10.1007/978-3-540-78800-3_30
[4]   Abstractions from proofs [J].
Henzinger, TA ;
Jhala, R ;
Majumdar, R ;
McMillan, KL .
ACM SIGPLAN NOTICES, 2004, 39 (01) :232-244
[5]  
JONSSON B, 1963, THEORY MODELS, P146
[6]  
KAPUR D, 2006, P 14 ACM SIGSOFT INT, P105
[7]  
McMillan KL, 2005, LECT NOTES COMPUT SC, V3440, P1
[8]  
McMillan KL, 2004, LECT NOTES COMPUT SC, V2988, P16
[9]  
McMillan KL, 2003, LECT NOTES COMPUT SC, V2725, P1
[10]  
Podelski A, 2007, LECT NOTES COMPUT SC, V4354, P245
12