Interval Temporal Logic Proofs
I Imperative Reasoning
proofs
1 A Proof System
1.1 Propositional Axioms and Inference
Rules
1.2 Propositional proofs
2 Propositional Interval Temporal
Logic Theorems
2.1 Basic ITL Theorems
2.2 Further
properties of Diamond-i and Box-i
2.3 Properties of Diamond-a
and Box-a
2.4 Properties of Fin
2.5 Properties of
chop-plus
2.6 Properties of chop-star
2.7 Properties of
While
2.8 Properties of Halt
2.9 Properties of groups
of chops
II JANCL proofs
3 Propositional Proofs
4 PITL Axiom
System
4.1 Axioms and Inference Rules for PITL
5 Deduction
of PTL Axioms from the FL Axiom System
III LMCS proofs
6 Axiom
system for PITL with finite and infinite time
7 Axiom system for PITL
with finite time
8 Some PITL theorems and Their Proofs
8.1 Some
Basic Properties of Chop
8.2 Some Properties of involving the
Modal System K and Axiom D
8.3 Some Properties of Chop,
and with State Formulas
8.4 Some Properties of involving the
Modal System K4
8.5 Properties Involving the PTL Operator
8.6 Some Properties of Together with
8.7 Some Properties
of Chop-Star
8.8 Some Properties Involving a Reduction to PITL
with Finite Time
8.9 Some Properties of Skip, Next And Until