A Complete Axiomatization of Propositional Projection Temporal Logic

This paper investigates a complete axiomatic system for propositional projection temporal logic (PPTL). To this end, the syntax, semantics, and logic laws of PPTL are briefly introduced. Further, the normal form of PPTL formulas is presented. Moreover, an axiomatic system of PPTL is formalized. A set of axioms and inference rules are given in details. To assist the proof within the system, some theorems are proved by means of the axioms and rules. In addition, based on the axioms, rules and theorems, the soundness and completeness of the deductive system are proved. Finally, an example is given to illustrate how the axiom system works.