A Complete Proof System for First Order Interval Temporal Logic with Projection

Research output: Contribution to journalArticle

Colleges, School and Institutes


This paper presents an omega-complete proof system for the extension of first-order Interval Temporal Logic (ITL) by a projection operator. Alternative earlier approaches to the axiomatisation of projection in ITL are briefly presented and discussed. An extension of the proof system which is complete for the extension of Duration Calculus (DC) by projection is also given.


Original languageEnglish
Pages (from-to)215-249
Number of pages35
JournalJournal of Logic and Computation
Issue number2
Publication statusPublished - 1 Apr 2004