Interpolation theorems for some variants of LTL
Interpolation theorems for some variants of LTL
Author(s): Norihiro KamideSubject(s): Philosophy, Logic
Published by: Wydawnictwo Uniwersytetu Jagiellońskiego
Summary/Abstract: 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.
Journal: Reports on Mathematical Logic
- Issue Year: 2015
- Issue No: 50
- Page Range: 3-30
- Page Count: 28
- Language: English