Design And Implementation Of Theorem Prover For First-order Logic Based On Sequent Calculus

The theorem prover is a computer program for proving mathematical theorems. The increasing requirement of formal verification for the computer hardware and software has brought out a wide variety of formal tools in recent decades. As an important tool of formal method, the theorem provers play an important role, which makes the study about them significant. However, slow progress has been made at home. This paper designs and implements a First-order Logic theorem prover named FolProver based on Sequent Calculus, which can be used to prove the correctness of theorems in First-order Logic.First of all, the theory related with First-order Logic and Sequent Calculus has been analyzed and introduced in details, which contains the syntax and semantics of First-order Logic, the inference rules of Sequent Calculus, and the soundness and completeness. Then this paper designs the architecture of FolProver, and presents its proof mechanism. In addition, the paper designs and implements all the modules contained in this theorem prover with F# and WPF, such as the lexical and syntax analyzation module, the primary inference rules module and so on. At last, some examples are demonstrated, which indicate that FolProver does a good job in usability and ease of use.The theorem prover implemented here is equipped with a graphic user interface and much helpful function, such as saving and loading a proof. The proof can be performed both interactively and automatically. In the future, rich built-in libraries can be realized, and relevant work can be done to support other logic systems on the basis of this paper, which can enhance FolProver.