Part 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

Proofs taken from

Ben C. Moszkowski. “Imperative Reasoning in Interval Temporal Logic”, Internal Report, University of Newcastle upon Tyne.

2023-09-12

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

© 1996-2023