A Sound and Complete Proof System for QPTL

Abstract

In this paper we give sound and complete proof systems for the useful and expressive quantified 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 efficient
complementation procedure for nondeterministic Buchi automata.

Full Paper

Postscript version of Early Draft of 2/8/01

Status

Draft in preparation. Short version submitted to a conference in August 2001.

Bibtex

@misc{FR:qptl:long,
author="T. French and M. Reynolds",
title="A Sound and Complete Proof System for QPTL",
year="2001",
note="in preparation"
}