ITL
© 1996-2018







6 Interval Temporal Algebra

Interval Temporal Algebra [Slide 23]

(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

Axiom/proof system for PITL [Slide 24]

PropAx
All axioms for propositional logic
ChopAssoc
(f0 ; f1) ; f2 f0 ; (f1 ; f2)
OrChopImp
(f0 f1) ; f2 (f0 ; f2) (f1 ; f2)
ChopOrImp
f0 ; (f1 f2) (f0 ; f1) (f0 ; f2)
EmptyChop
empty ; f1 f1
ChopEmpty
f1 ; empty f1
BiBoxChop
(f0 f1) (f2 f3) (f0 ; f2) (f1 ; f3)
StateImpBi
p p
NextImpWNext
f0 ¬¬f0
SkipAnd
(skip f0) ; true ¬((skip ¬f0) ; true)
BoxInduct
f0 (f0 ¬¬f0) f0
ChopStarEqv
f0 (empty ((f0 more) ; f0))
ChopStarInduct
(inf f0 (f0 (f1 fmore) ; f0)) f1
MP
f0 f1 and f0 implies f1
BoxGen
f0 implies f0
BiGen
f0 implies f0

Examples of proof in ITA [Slide 25]

Example 1.  

finite Σ
use a Σ = a
=
finite

Example 2.  

(T )
use a (b c) = (a b) c
=
T ()
use a =
=
T

ITA vs PITL [Slide 26]

Theorem 3. PITL is an interval temporal algebra

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







2018-02-26
Contact | Home | ITL home | Course | Proofs | Algebra | FL