(K,ω) is an interval temporal algebra iff
Let skip ≜∼(Σ ∪∼Σ ⋅∼Σ), finite ≜∼(T ⋅∅) and a ≜∼(finite ⋅∼a)
(K,ω) is a Boolean left (lazy) omega algebra
a ⋅ (b ∪c) ⊆a ⋅b ∪a ⋅c
(skip ∩a) ⋅c ∩ (skip ∩b) ⋅d = (skip ∩a ∩b) ⋅ (c ∩d)
c ⋅ (skip ∩a) ∩d ⋅ (skip ∩b) = (c ∩d) ⋅ (skip ∩a ∩b)
(Σ ∩a) ⋅c ∩ (Σ ∩b) ⋅d = (Σ ∩a ∩b) ⋅ (c ∩d)
c ⋅ (Σ ∩a) ∩d ⋅ (Σ ∩b) = (c ∩d) ⋅ (Σ ∩a ∩b)
finite ⊆skip∗
∼(skip ⋅∼a) = Σ ∪skip ⋅a
∼(∼a ⋅skip) = Σ ∪a ⋅skip
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 |