Interval Temporal Logic Proofs

Antonio Cau, Ben Moszkowski and David Smallwood

Pdf version of Interval Temporal 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

Contact | Home | ITL home | Course | Proofs | Algebra | FL
© 1996-2023