A complete axiomatic characterization of first-order temporal logic of linear time (Q1102941)

This paper deals with the theory of first order temporal logic of linear and discrete time (FOTLL), with the ``atnext'' operator A instead of the ``until'' operator U. An infinitary, sound and complete proof system for FOTLL is given (it is known that no such finitary system could exist). The proof method is based on Q-filters (adopted from algorithmic logic). It is also proved that any syntactically consistent temporal theory has a model. An example of the use of an infinitary proof rule in proving correctness of a concurrent version of Quicksort is provided.