ITL
© 1996-2015







6 Interval Temporal Algebra

(K, ω) is an interval temporal algebra iff

Let        ---------
skip=^ Σ ∪ Σ-⋅Σ- ,    finite ^= T-⋅∅ and !a ^= finite-⋅a-

P1
(K, ω) is a Boolean left (lazy) omega algebra
P2
a ⋅(b∪ c) ⊆ a ⋅b∪ a ⋅c
P3
(skip ∩ a) ⋅c∩ (skip ∩ b)⋅d = (skip ∩ a∩ b) ⋅(c∩ d)
P4
c ⋅(skip ∩ a)∩ d ⋅(skip ∩b) = (c∩ d) ⋅(skip ∩ a∩ b)
P5
(Σ ∩ a) ⋅c∩ (Σ ∩ b)⋅ d= (Σ ∩ a ∩ b)⋅(c ∩ d)
P6
c ⋅(Σ ∩ a)∩ d ⋅(Σ ∩ b)= (c ∩ d)⋅(Σ ∩ a ∩ b)
P7
finite ⊆ skip*
P8
-------
skip⋅a = Σ ∪ skip⋅a
P9
a-⋅skip-= Σ ∪ a ⋅skip
PropAx        A llaxiomsforpropositionallogic
C hopA ssoc     ⊢ (f0 ;f1);f2 ≡ f0 ;(f1 ;f2)
O rC hopIm p    ⊢ (f0 ∨ f1);f2 ⊃ (f0 ;f2) ∨ (f1 ;f2)
C hopO rIm p    ⊢ f0 ;(f1 ∨ f2) ⊃ (f0 ;f1) ∨ (f0 ;f2)
E mptyC hop    ⊢ em pty;f1 ≡ f1
C hopE mpty    ⊢ f1 ;em pty ≡ f1
B iBoxC hop    ⊢ I (f0 ⊃ f1) ∧ ! (f2 ⊃ f3) ⊃ (f0 ;f2) ⊃ (f1 ;f3)
StateImpB i    ⊢ p ⊃  I p
N extImpW Next ⊢ C f0 ⊃  C f0
SkipAnd       ⊢ (skip ∧ f0) ;true ⊃  ((skip ∧ f0 );true )
B oxInduct     ⊢ f0 ∧ ! (f0 ⊃  C f0) ⊃  !f0
C hopS tarEqv   ⊢ f *0 ≡ (e mpty ∨ ((f0 ∧ more); f*0))
C hopS tarInduct ⊢ (inf ∧ f0 ∧ !(f0 ⊃ (f1 ∧ fm ore) ;f0)) ⊃ f*1
M P           ⊢ f0 ⊃ f1 and ⊢ f0 implies ⊢ f1
B oxGen       ⊢ f0 im plies ⊢ !f0
B iG en         ⊢ f0 im plies ⊢ If0

Example 1

   finite ⋅Σ
   — a ⋅Σ = a
=  finite

_____________________________________________________________________

Example 2

    (T ⋅∅)⋅∅
    — a ⋅(b⋅c) = (a⋅b) ⋅c
=   T ⋅(∅⋅∅)
    — ∅ ⋅a=  ∅
=   T ⋅∅

_____________________________________________________________________

Theorem 1 PITL is an interval temporal algebra

_____________________________________________________________________

Theorem 2 PITL’s axiom/proof system can be derived from ITA’s axiom system

_____________________________________________________________________