A sound and complete proof system for QPTL
Tim French, Mark A Reynolds · UWA Profiles and Research Repository (UWA) · 2002
this paper we give sound and complete proof systems for the useful and expressive quanti ed propositional temporal logic, both with and without past temporal operators. Until now an axiomatization has only existed for the version with the inclusion of the past operators and this axiomatization relied on the past operators in subtle and complicated ways. In certain situations, such as in branching time extensions of the linear time logic, it is important to avoid using the past time operators. Our completeness proof proceeds mostly by using deterministic Rabin automata but the main step is via a new and interesting proof of correctness for an optimal complementation procedure for nondeterministic Buchi automata