Ben Moszkowski - A Complete Axiom System for Propositional Interval Temporal Logic with Infinite Time

lmcs:759 - Logical Methods in Computer Science, August 13, 2012, Volume 8, Issue 3 - https://doi.org/10.2168/LMCS-8(3:10)2012
A Complete Axiom System for Propositional Interval Temporal Logic with Infinite TimeArticle

Authors: Ben Moszkowski

    Interval Temporal Logic (ITL) is an established temporal formalism for reasoning about time periods. For over 25 years, it has been applied in a number of ways and several ITL variants, axiom systems and tools have been investigated. We solve the longstanding open problem of finding a complete axiom system for basic quantifier-free propositional ITL (PITL) with infinite time for analysing nonterminating computational systems. Our completeness proof uses a reduction to completeness for PITL with finite time and conventional propositional linear-time temporal logic. Unlike completeness proofs of equally expressive logics with nonelementary computational complexity, our semantic approach does not use tableaux, subformula closures or explicit deductions involving encodings of omega automata and nontrivial techniques for complementing them. We believe that our result also provides evidence of the naturalness of interval-based reasoning.


    Volume: Volume 8, Issue 3
    Published on: August 13, 2012
    Imported on: May 25, 2011
    Keywords: Computer Science - Logic in Computer Science,F.4.1, F.3.1

    7 Documents citing this article

    Consultation statistics

    This page has been seen 1045 times.
    This article's PDF has been downloaded 359 times.