TY - JOUR
TI - Interpolation theorems for some variants of LTL
AU - Kamide, Norihiro
TI - Interpolation theorems for some variants of LTL
AB - It is known that Craig interpolation theorem does not hold for LTL. In this paper, Craig interpolation theo- rems are shown for some fragments and extensions of LTL. These theorems are simply proved based on an embedding-based proof method with Gentzen-type sequent calculi. Maksimova separation theorems (Maksimova principle of variable separation) are also shown for these LTL variants.
VL - 2015
IS - Number 50
PY - 2015
SN - 0137-2904
C1 - 2084-2589
SP - 3
EP - 30
DO - 10.4467/20842589RM.15.001.3910
UR - https://ejournals.eu/en/journal/reports-on-mathematical-logic/article/interpolation-theorems-for-some-variants-of-ltl
KW - paraconsistent logic
KW - sequent calculus
KW - Craig interpolation theorem
KW - linear-time temporal logic
KW - infinitary logic