School of Computing

Constructive interval temporal logic in Alf

Simon Thompson

In International Conference on Temporal Logic 1997, Applied Logic, pages 182-196. Kluwer, January 1997 These proceedings are to be publised by Kluwer in 1997.


This paper gives an implementation of an interval temporal logic in a constructive type theory, using the Alf proof system. After explaining the constructive approach, its relevance to interval temporal logic and potential applications of our work, we explain the fundamentals of the Alf system. We then present the implementation of the logic and give a number of examples of its use. We conclude by exploring how the work can be extended in the future.

Download publication 178 kbytes (PostScript)

Bibtex Record

author = {Simon Thompson},
title = {Constructive interval temporal logic in {A}lf},
month = {January},
year = {1997},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {These proceedings are to be publised by Kluwer in 1997.},
doi = {},
url = {},
    booktitle = {International Conference on Temporal Logic 1997},
    publisher = {Kluwer},
    refereed = {yes},
    series = {Applied Logic},

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 21/03/2014