Oxford Journals
tools journals homepage advanced search contact help
Journal of Logic and Computation: Current Issue

OUP > Journals > Computing/Engineer. & Mathematics/Stats. > Journal of Logic and Computation

Journal of Logic and Computation

Volume 13, Issue 2, April 2003: pp. 195-239

A Decision Procedure and Complete Axiomatization of Finite Interval Temporal Logic with Projection

Howard Bowman1 and Simon Thompson1

1Computing Laboratory, University of Kent at Canterbury, Canterbury, Kent, CT2 7NF. E-mail: {H.Bowman,S.J.Thompson}@ukc.ac.uk

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 formluae. 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.

Keywords: Tableau; temporal; decision procedure; interval; chop; projection; normal form; complete axiomatization

Table of Contents   Full-Text PDF (263 KB)

Oxford University Press
Published by Oxford University Press
Copyright ©Oxford University Press 2003
Print ISSN: 0955-792X  Online ISSN: 1465-363X.
Oxford University Press Privacy Policy and Legal Statement