Implementation Of A Theorem Prover For PPTL With Indexed Expressions

In the design of modern computer systems,errors occur frequently and endlessly.Formal verification is an effective approach to ensure the correctness of systems and is widely used in safety-critical fields with high-reliability requirements.Model checking and theorem proving are two main formal verification methods.The advantage of theorem proving is the strong abstract ability which makes the verification not limited by the scale of systems to be verified and avoids the state space explosion problem.While the disadvantage is the low degree of automation and high requirements for users’ mathematical literacy.Interactive theorem proving can assist the proof process,realize the semi-automatic proof under manual guidance and ensure the correctness of the proof.Propositional Projection Temporal Logic(PPTL)with indexed expressions is an extension of PPTL with full regular expressiveness.It can express the infinite loop structure formulas more concisely,becomes a superset of Linear Temporal Logic(LTL),and has great potential for formal verification of infinite loop systems.In addition,a sound and complete proof system for PPTL with indexed expressions has been developed for theorem proving.However,proving merely in a manual approach leads to a low degree of automation and a high probability of proof lapse.Aiming at the above problems,it is a reasonable solution to formalize the PPTL axiom system with indexed expressions and then realize interactive theorem proving in the interactive theorem prover Coq.To improve the automation of theorem proving of PPTL with indexed expressions,this thesis studies the method of formalizing the proof system for PPTL with indexed expressions in Coq,then designs and implements a theorem prover for PPTL with indexed expressions.Firstly,the framework of the theorem prover is designed,including the formalization of the PPTL proof system with indexed expressions and interactive theorem proving.Then,the formalization part of this theorem prover is realized.The first step is the formalization of basic formulas,derived formulas,and indexed expressions.The second step is the definition of the deduction relationship.The third step is the coding of two proof sub-systems for both basic formulas and indexed expressions.Finally,the theorem prover is applied in the following aspects: the proof of basic formula theorems and theorems with indexed expressions,and the modeling and verification of a mutual exclusion mechanism.The above examples demonstrate that the theorem prover is relatively practical.It can not only be applied to the definition and extension of the proof system of PPTL with indexed expressions,but also the theorem proving of actual systems.