Richard Zach
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
