Completeness of a first-order temporal logic with time-gaps

Theoretical Computer Science 160 (1-2):241-270 (1996)
  Copy   BIBTEX


The first-order temporal logics with □ and ○ of time structures isomorphic to ω (discrete linear time) and trees of ω-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.

Author Profiles

Richard Zach
University of Calgary


Added to PP

371 (#43,529)

6 months
74 (#54,928)

Historical graph of downloads since first upload
This graph includes both downloads from PhilArchive and clicks on external links on PhilPapers.
How can I increase my downloads?