A hierarchical completeness proof for propositional temporal logic
This paper introduces novel analysis of conventional propositional linear-time temporal logic (PTL). Two key features of the method are that it is hierarchical and an interval-oriented generalization of PTL called PITL serves as a kind of meta-notation. The presentation concerns axiomatic completeness for PTL but is further developed in Outputs 3 and 4 to consider numerous issues. Consequently, the significance and impact from those papers (including a BCS-FACS seminar and a Belgian national seminar) also reflects on this one which initiated the approach.
Citation : Moszkowski, B.C.(2004) A hierarchical completeness proof for propositional temporal logic.In: Dershowitz N. (eds) Verification: Theory and Practice. Lecture Notes in Computer Science, vol 2772. Springer, Berlin, Heidelberg.
ISSN : 0302-9743
Research Group : Software Technology Research Laboratory (STRL)