University of Calgary
UofC Navigation

A complete first-order temporal logic of time with gaps

This website has moved!

You are looking at an archived page. The website has moved to richardzach.org.

Source

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

Abstract

The first-order temporal logics with ? and ? 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.

Download from Elsevier ScienceDirect

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

Download preprint

Download PostScript