A complete proof system for propositional projection temporal logic (2013)

Author(s): Duan Z, Zhang N, Koutny M

    Abstract: The paper presents a proof system for Propositional Projection Temporal Logic (PPTL) with projection-plus. The syntax, semantics, and logical laws of PPTL are introduced together with an axiom system consisting of axioms and inference rules. To facilitate proofs, some of the frequently used theorems are proved. A normal form of PPTL formulas is presented, and the soundness and completeness of the proof system are demonstrated. To show how the axiom system works, a full omega regular property for the mutual exclusion problem is specified by a PPTL formula and then a deductive proof of the property is performed.

      • Legacy Date: 29/07/2013
      • Journal: Theoretical Computer Science
      • Volume: 497
      • Pages: 84-107
      • Publisher: Elsevier BV
      • Publication type: Article
      • Bibliographic status: Published

      Keywords: Temporal logic; Axiomatization; Soundness; Completeness; Inference rule


      Professor Maciej Koutny
      CS Director of Research