| | Interval Temporal Logic Proofs
Antonio Cau, Ben Moszkowski and David Smallwood
I Imperative Reasoning proofs
1 A Proof System
1.1 Propositional Axioms and Inference Rules
1.2 First-Order Axioms and Inference Rules
2 Propositional proofs
3 Derived proof system for chop-free temporal logic
4 Further properties of Diamond-i and Box-i
5 Properties of Diamond-a and Box-a
6 Properties of Fin
7 Properties of chop-plus
8 Properties of chop-star
9 Properties of While
10 Properties of Halt
11 Properties of groups of chops
II JANCL proofs
12 Propositional Proofs
13 PITL Axiom System
13.1 Axioms and Inference Rules for PITL
14 Deduction of PTL Axioms from the FL Axiom System
III LMCS proofs
15 Axiom system for PITL with ﬁnite and inﬁnite time
16 Axiom system for PITL with ﬁnite time
17 Some PITL theorems and Their Proofs
17.1 Some Basic Properties of Chop
17.2 Some Properties of involving the Modal System K and Axiom D
17.3 Some Properties of Chop, and with State Formulas
17.4 Some Properties of involving the Modal System K4
17.5 Properties Involving the PTL Operator
17.6 Some Properties of Together with
17.7 Some Properties of Chop-Star
17.8 Some Properties Involving a Reduction to PITL with Finite Time
17.9 Some Properties of Skip, Next And Until
| | |