Simplification Method for Contradiction Separation Clause in First-order Logic AutomatedTheorem Prover CSE

Abstract

First-order logic automated theorem proving has the capacity to resolve a multitude of practical problems after formalization,and thus holds considerable practical value.As an advancement in automated theorem proving,contradiction separation deduction extends the classical resolution principle and exhibits enhanced proving capability.In this paper,a simplified algorithm for contradiction separation is proposed and theoretically proven based on the Contradiction Separation Extension(CSE) prover,which follows the rule of contradiction separation.The proposed algorithm enhances efficiency via data structure optimization,utilizing pointers to store complementary information between clauses.This information is then employed to select the clauses that are involved in deductions,thereby achieving the separation clause simplification.This approach produces shorter separation clauses while leveraging the unification complementarity of clauses to strengthen the detection capability of empty clause derivation paths,ultimately improving prover efficiency.Experimental results demonstrate that the enhanced prover CSE_BSCS with this simplification algorithm solves 39 additional test cases compared to the original CSE,with an 18.64% reduction in average proving time. These improvements confirm the superior performance of CSE_BSCS in both proving capability and efficiency over CSE.

Keywords

• contradiction separation|contradiction separation simplification|separation clause simplification|complementary information|prover