A hierarchical completeness proof for propositional Interval Temporal Logic with finite time
Interval-oriented temporal logics are now found even in three recent IEEE standards. Consequently, it is natural to better understand the proof theory, including completeness. We describe a propositional axiom system adapted from our previous work and a completeness proof which involves a hierarchical reduction to conventional temporal logic and is much more direct than previous proofs (e.g., with tableaux). Future presentations of such logics’ proof theory will cite this. It will also encourage more hierarchical analyses. An unexpected spinoff is an intermediate interval-oriented logic with theoretical and practical value, including an implementable symbolic decision procedure (Theoretical Computer Science, Vol. 337, 2005).
Citation : Moszkowski, B.C. (2004) A hierarchical completeness proof for propositional Interval Temporal Logic with finite time. Journal of Applied Non-Classical Logics, 14 (1-2), pp.55-104.
ISSN : 1166-3081
Research Group : Software Technology Research Laboratory (STRL)