School of Computing

A Complete Axiomatization of Interval Temporal Logic with Projection

Howard Bowman and Simon Thompson

Technical Report 6-00, Computing Laboratory, University of Kent, January 2000.

Abstract

This paper presents a complete axiomatisation for propositional interval temporal logic (PITL) with projection. The axiomatisation is based on a tableau procedure for the logic, which in turn is founded upon a normal form for PITL formluae.

The construction of the axiomatisation is modular, in the sense that given a normal form for a new connective, axioms can be generated for the connective from the tableau construction. The paper concludes with a discussion of aspects of compositionality for PITL with projection.

Download publication 632 kbytes (PostScript)

Bibtex Record

@techreport{960,
author = {Howard Bowman and Simon Thompson},
title = {{A Complete Axiomatization of Interval Temporal Logic with Projection}},
month = {January},
year = {2000},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/2000/960},
    institution = {Computing Laboratory, University of Kent},
    number = {6-00},
    publication_type = {techreport},
    submission_id = {22866_948883504},
    type = {Technical Report},
}

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

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

Last Updated: 21/03/2014