Logical Interpolation and Projection onto State in the Duration Calculus

Journal of Applied Non-Classical Logics 14 (1-2):181-208 (2004)
  Copy   BIBTEX


We generalise an interval-related interpolation theorem about abstract-time Interval Temporal Logic, which was first obtained in [GUE 01]. The generalisation is based on the abstract-time variant of a projection operator in the Duration Calculus, which was introduced in [DAN 99] and later studied extensively in [GUE 02]. We propose a way to understand interpolation in the context of formal verification. We give an example showing that, unlike abstract-time ITL, DC does not have the Craig interpolation property in general, and establish a special form of Craig interpolation for abstract-time DC. Explicit definability after Beth is known to be strongly related to Craig interpolation in general. We show a limitation of a different kind to the scope of Beth definability in ITL by a counterexample too. We call the generalisation of interval-related interpolation that we present projection-related interpolation. The DC-specific restrictions apply to it too. We show that both Craig and projection-related interpolation hold about the ⌈P⌉-subset of DC without such restrictions. Our proofs of these theorems for the ⌈P⌉-subset entail algorithms for the construction of the interpolants.



    Upload a copy of this work     Papers currently archived: 84,049

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Is there really no projection postulate in the modal interpretation?W. Michael Dickson - 1995 - British Journal for the Philosophy of Science 46 (2):197-218.
Limitations of the projection postulate.L. E. Ballentine - 1990 - Foundations of Physics 20 (11):1329-1343.
Interpolation in fragments of classical linear logic.Dirk Roorda - 1994 - Journal of Symbolic Logic 59 (2):419-444.
Notes on Craig interpolation for LJ with strong negation.Norihiro Kamide - 2011 - Mathematical Logic Quarterly 57 (4):395-399.


Added to PP

36 (#350,673)

6 months
1 (#510,366)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

No citations found.

Add more citations

References found in this work

Model Theory.Gebhard Fuhrken - 1976 - Journal of Symbolic Logic 41 (3):697-699.
Interpolation for first order S5.Melvin Fitting - 2002 - Journal of Symbolic Logic 67 (2):621-634.
Constructive interpolation in hybrid logic.Patrick Blackburn & Maarten Marx - 2003 - Journal of Symbolic Logic 68 (2):463-480.

View all 6 references / Add more references