© University of Kent - Contact | Feedback | Legal | FOI | Cookies
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}, }