School of Computing

A decision procedure and complete axiomatization of finite interval temporal logic with projection

H. Bowman and S.J. Thompson

Journal of Logic and Computation, 13(2):182-196, April 2003.

Abstract

This paper presents a complete axiomatization for propositional interval temporal logic (PITL) with projection. The axiomatization is based on a tableau decision procedure for the logic, which in turn is founded upon a normal form for PITL formulae. The construction of the axiomatization provides a general mechanism for generating axiomatizations thus: given a normal form for a new connective, axioms can be generated for the connective from the tableau construction using that normal form. The paper concludes with a discussion of aspects of compositionality for PITL with projection.



Bibtex Record

@article{1604,
author = {H. Bowman and S.J. Thompson},
title = {A Decision Procedure and Complete Axiomatization of Finite Interval Temporal Logic with Projection},
month = {April},
year = {2003},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/2003/1604},
    publication_type = {article},
    submission_id = {26518_1049386365},
    journal = {Journal of Logic and Computation},
    volume = {13},
    number = {2},
    publisher = {Oxford University Press},
    ISSN = {0955-792X},
}

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

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

Last Updated: 21/03/2014