A complete first-order temporal logic of time with gaps


Theoretical Computer Science 160 (1996) 241-270
(with Matthias Baaz and Alexander Leitsch)

The first-order temporal logics with \(\Box\) and \(\bigcirc\) of time structures isomorphic to \(\omega\) (discrete linear time) and trees of \(\omega\)-segments (linear time with branching gaps) and some of its fragments are compared: The first is not recursively axiomatizable. For the second, a cut-free complete sequent calculus is given, and from this, a resolution system is derived by the method of Maslov.

DOI: 10.1016/0304-3975(95)00107-7


Leave a Reply

Your email address will not be published. Required fields are marked *