© 1996-2018

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 finite and infinite time
16 Axiom system for PITL with finite 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

Contact | Home | ITL home | Course | Proofs | Algebra | FL