Holistic deductive framework theorem proving based on standard contradiction separation for first-order logic

摘要

Nowadays, famous and powerful first-order logic automated theorem proving almost use saturation which called given-clause algorithm as the deductive framework. The given-clause algorithm is a divisional framework which divides the entire clauses into selected clause set and deductive clause set. It is efficient with large heuristic strategies and inference calculus. In this paper, we present a holistic deductive framework based on standard contradiction separation. The framework allows arbitrary clause to take part in deduction in the holistic clause set as many as possible which can take full advantage of synergetic effect between clauses. It is a multi-ary, dynamic, sound, complete deduction which can generate more new unit clauses as the goal. We implement the preliminary version of prover, it can find proofs in fewer inferential steps for some Mizar and TPTP problems under effective strategies. Related definitions and useful methods are proposed for programming search paths, avoiding repetition, simplifying clauses and the key strategies, they are contribute to finding proof more efficiently. Performance analysis and some conclusions are outlined at the end of this paper.