### 6 Interval Temporal Algebra

#### Interval Temporal Algebra [Slide 23]

(K,ω) is an interval temporal algebra iﬀ

Let skip (Σ Σ Σ),    ﬁnite (T ) and a (ﬁnite 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
ﬁnite 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.

 ﬁnite ⋅Σ use a ⋅Σ = a = ﬁnite

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