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
关键词
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 条
  • [1] Abreces C., 2001, CSLI LECT NOTES, P35
  • [2] [Anonymous], REPORTS MATH LOGIC
  • [3] [Anonymous], 1983, SYNTHESE LIB
  • [4] [Anonymous], 1960, SUGAKU
  • [5] Bicarregui J., 2001, Log. J. IGPL, V9, P231, DOI [10.1093/jigpal/9.2.231, DOI 10.1093/JIGPAL/9.2.231]
  • [6] CARBONE A, 1996, COLLEGIUM LOGICUM, V2, P87
  • [7] Preservation of interpolation features by fibring
    Carnielli, Walter
    Rasga, Joao
    Sernadas, Cristina
    [J]. JOURNAL OF LOGIC AND COMPUTATION, 2008, 18 (01) : 123 - 151
  • [8] Craig William, 1957, J. Symb. Log., V22, P250
  • [9] Czelakowski J, 1999, LECT NOTES PURE APPL, V203, P187
  • [10] Gabbay D., 2011, CONDITIONALS MODULAR