LMCS proofs

6 Axiom system for PITL with ﬁnite and inﬁnite time

7 Axiom system for PITL with ﬁnite 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

7 Axiom system for PITL with ﬁnite 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

Proofs taken from

Ben C. Moszkowski. “A Complete Axiom System for Propositional Interval Temporal Logic with Inﬁnite Time”. In: Logical Methods in Computer Science Journal 8.3 (2012). url.