一个用于一阶逻辑自动定理证明的新算法

本文提出一个用于一阶逻辑(FOPC)自动定理证明的并行算法,它基于分治的思想,把原问题子句集S划分成两个独立的子句集S1和S2,并通过并行地证明S_1和S_2的不可满足性。本文首先讨论了子句集的划分问题,引入了导出子句集及划分因子的概念;然后,在此基础上,提出了FOPC定理证明的并行算法;最后,给出了算法的有效性和完备性证明。文中还讨论了子句集的化简及算法性能评价等问题。

A New Method For Automated Theorem Proving in First Order Predicate Calculus (FOPC)

In this paper,a parallel algorithm for automated theorem proving in FOPC is proposed. This algorithm, based on the divide-and-conquer strategy,divides the original problem in to two independent subproblems that can be processed in parallel. First,the dividing method of a setof clauses is discussed; then, based on the.dividing method, the parallel algorithm for theorem proving in FOPC is presented;finally,the soundness and completeness of the algorithm are proved.In addition,the simplification of a set of clauses and the performance of the algorithm are also discussed.