Preservation of Craig interpolation by the product of matrix logics

被引：3
作者：
Sernadas, C. [1 ,2 ]
Rasga, J. [1 ,2 ]
Sernadas, A. [1 ,2 ]
机构：
[1] Univ Lisbon, Inst Super Tecn, Dep Matemat, P-1699 Lisbon, Portugal
[2] Inst Telecomunicacoes, SQJG, Lisbon, Portugal
来源：
JOURNAL OF APPLIED LOGIC | 2013年 / 11卷 / 03期
关键词：
Interpolation; Matrix semantics; Matrix-logic product;
D O I：
10.1016/j.jal.2013.06.001
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
The product of matrix logics, possibly with additional interaction axioms, is shown to preserve a slightly relaxed notion of Craig interpolation. The result is established symbolically, capitalizing on the complete axiomatization of the product of matrix logics provided by their meet-combination. Along the way preservation of the metatheorem of deduction is also proved. The computation of the interpolant in the resulting logic is proved to be polynomially reducible to the computation of the interpolants in the two given logics. Illustrations are provided for classical, intuitionistic and modal propositional logics. (C) 2013 Elsevier B.V. All rights reserved.
引用
收藏
页码：328 / 349
页数：22
相关论文
共 21 条
  • [11] Gabbay D. M., 2005, Interpolation and definability. Modal and intuitionistic logics, V46
  • [12] Gabbay Dov M., 1972, P C MATH LOG LOND, P111
  • [13] INTERPOLANT-BASED TRANSITION RELATION APPROXIMATION
    Jhala, Ranjit
    McMillan, Kenneth L.
    [J]. LOGICAL METHODS IN COMPUTER SCIENCE, 2007, 3 (04)
  • [14] PROPERTIES OF INDEPENDENTLY AXIOMATIZABLE BIMODAL LOGICS
    KRACHT, M
    WOLTER, F
    [J]. JOURNAL OF SYMBOLIC LOGIC, 1991, 56 (04) : 1469 - 1485
  • [15] Marx M., 1998, Notre Dame Journal of Formal Logic, V39, P253, DOI 10.1305/ndjfl/1039293067
  • [16] An interpolating theorem prover
    McMillan, KL
    [J]. THEORETICAL COMPUTER SCIENCE, 2005, 345 (01) : 101 - 121
  • [17] Miller C, 2010, LECT NOTES COMPUT SC, V6175, P194, DOI 10.1007/978-3-642-14186-7_17
  • [18] Mundici D., 1984, LOG C 82, V112, P345
  • [19] Schumm G.F., 1986, NOTRE DAME J FORM L, V27, P108
  • [20] On meet-combination of logics
    Sernadas, A.
    Sernadas, C.
    Rasga, J.
    [J]. JOURNAL OF LOGIC AND COMPUTATION, 2012, 22 (06) : 1453 - 1470
123