Interpolation for intermediate logics via injective nested sequents

被引：1

作者：

Kuznets, Roman ^{[1
]}

Lellmann, Bjoern ^{[1
]}

机构：

[1] TU Wien, Vienna, Austria

来源：

JOURNAL OF LOGIC AND COMPUTATION | 2021年 / 31卷 / 03期

基金：

奥地利科学基金会;

关键词：

CALCULI;

D O I：

10.1093/logcom/exab015

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

We introduce a novel, semantically inspired method of constructing nested sequent calculi for propositional intermediate logics. Applying recently developed methods for proving Craig interpolation to these nested sequent calculi, we obtain constructive proofs of the interpolation property for most non-trivial interpolable intermediate logics, as well as Lyndon interpolation for Godel logic. Finally, we provide a prototype implementation combining proof search and countermodel construction.

引用

页码：797 / 831

页数：35

共 28 条

[1]

[Anonymous], 1999, Logic Journal of the IGPL, DOI DOI 10.1093/JIGPAL/7.3.319

[2]

Avellone A., 1999, LOG J IGPL, V7, P447, DOI [10.1093/jigpal/7.4.447, DOI 10.1093/JIGPAL/7.4.447]

[3] On Interpolation in Automated Theorem Proving [J].