Study On A First-order Logic Automated Theorem Prover Based On Contradiction Separation Deduction

Automated reasoning is an important part of artificial intelligence,which mainly includes propositional logic solution and first-order logic theorem proving.First-order logic system has more expressive power than propositional logic system.Many problems in reality can be represented by first-order logic.Therefore,the research on the first-order logic automated theorem prover has important academic value and broad application prospects.At present,the first-order logic automated theorem provers generally adopt the saturation algorithm as deduction framework and the binary resolution methods as core inference mechanism.The saturation algorithm is a local deduction framework,and the performance of clause selection has a great dependence on heuristic strategy.The binary resolution methods limit only two clauses are involved,and only a complementary pairs of literals are eliminated in each resolution step.As a consequence,the generated clause usually has many literals,and there is potential room for improving this elegant inference mechanism.The contradiction separation rule is a multi-clause deduction method proposed by Professor Yang Xu.This method has a lot of excellent deduction characteristics and breaks through the limition of the traditional binary resolution methods,which only two clauses are involved and only a complementary pairs of literals are eliminated in each resolution step.In this dissertation,the components,system construction,deduction correctness verification and experimental results evaluation of the first-order logic automated theorem prover based on the contradiction separation theory are studied,and the whole system of the first-order logic automated theorem proving is designed and implemented,which contains the first-order logic automated theorem prover based on the contradiction separation deduction,the first-order logic automated theorem proving combined systems based on the contradiction separation deduction,and the first-order logic automated theorem proving verification tool.In the aspect of contradiction separation theory,a clause reduction rule of contradiction separation deduction is proposed,which can effectively reduce clause by analyzing the deduction features,and the soundness of the rule is proven.Several contradiction separation deduction methods have proposed,which can reduce the path search space.In the aspect of the preprocessing method of first-order logic clause set,the existing clause set preprocessing techniques used in current provers are generally only from the perspective of the symbol relevance,a preprocessing method of first-order logic clause set based on deduction distance between literals is proposed,which can effectively reduce the scale of clause set.The method is applied to the prover Vampire(champion of international prover competition),which can improve the capability of Vampire to a certain extent.The heuristic strategy based on contradiction separation deduction is studied.By analyzing the path search decision in the process of contradiction separation deduction,clause selection strategy,literal selection strategy,standard contradiction separation clause evaluation strategy,and standard contradiction separation deduction control strategy are proposed,which can effectively optimize contradiction separation deduction path search.Based on different path search schemes,three effective contradiction separation deduction algorithms are proposed,which are called the contradiction separation deduction algorithm based on the preferred clauses,the contradiction separation deduction algorithm based on the optimized deduction path,and the contradiction separation deduction algorithm based on the full use of clauses.In the process of deduction,the preferred path can be searched through the backtracking mechanism,thereby improving the efficiency of the path search.In the process of theorem proving,a path search algorithm based on the iterative deduction of starting clause is proposed,which effectively plans the search path of the contradiction separation deduction,and can improve the adequacy of the clauses to participate in contradiction separation deduction.A first-order logic automated theorem prover(called CSE)based on contradiction separation deduction is designed and implemented,and officially released three versions(called CSE 1.0,CSE 1.1 and CSE 1.2)that comply with the international standards,and have participated in the international first-order logic automated theorem proving systems competition in the last two years,where their performance exceed the well-known prover Prover9.CSE can be used to automatically solve first-order logic theorems,supporting command line running mode and visual running mode,and supporting multiple use of strategies.Taking the theorems from TPTP as the test object,CSE outperformed many wellknown first-order logic automated theorem provers,and can solve some theorems which unsolved by other provers.The combined methods of CSE and other provers are studied,and two combined methods are proposed for solving first-order logic theorems with different difficulty coefficients.The first-order logic automated theorem prover Vampire(champion of international prover competition)and Eprover(Second place in international prover competition)are selected and two combined systems CSE?V and CSE?E have designed.CSE?E has participated in the international first-order logic automated theorem proving systems competition in 2018 and won the second places in FOF division.The two combined systems support for unsatisfiable problems and satisfyable problem solving.Taking the theorems from CASC as the test object,both CSE?V and CSE?E outperformed Vampire and Eprover to a certain extent respectively.In addition,CSE?V and CSE?E solve some theorems with Rating of 1.The deduction process verification methods of CSE and CSE combined systems are studied.Two verification tools for CSE and CSE combined systems are designed and implemented,which effectively guarantee the correctness of deduction.