Design And Implementation Of First-Order Logic Theorem Prover Based On Sequent Calculus And Superposition

With the increasing requirements of the security and reliability of computer system,formal methods got more attention from the developer.Theorem Prover,which is one of the important technologies in formal methods,is a tool for proving mathematical theorems.With the help of theorem prover,users can prove theorems in a convenient and credible way.In this paper,we design and implement a theorem prover for First-Order Logic,which uses Sequent Calculus as its deductive system for interactive theorem proving and use Superposition for automated theorem proving.First of all,we introduce the theory of First-Order Logic and Ordering in preparation for the next chapter.Then we give a detailed description of three different deductive systems-Sequent Calculus,Resolution and Superposition.After that,we represent the function and the relation between each module in prover,then we introduce the design and implementation of each module from the perspective of interactive theorem proving and automatic theorem proving.Finally,we demonstrate the prover's functions in several cases and test the capabilities of this prover with a problem set.With the help of this prover we implemented,users can proof theorem interactively in the graphical interface,and can call the automated proving interface to try to solve the problem automatically,can also solve problems through cooperation between interactive and automated styles.In the future,one can extend this prover by supporting logic which has a more powerful expression or enhance the capabilities of automated theorem proving.