Interpolation theorems for some variants of LTL
Norihiro Kamide · Reports on Mathematical Logic · 2015
A b s t r a c t. It is known that Craig interpolation theorem does not hold for LTL. In this paper, Craig interpolation theorems 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.