Application of Multi-Clause Synergized Deduction in First-Order Logic Automated Theorem Proving

First-order logic is an important branch in mathematical logic, and automated reasoning of its logical formula is one of the important research hotspots in the field of artificial intelligence. Most of the state of the art first-order logic automated theorem proving systems adopt binary resolution method. There are only two clauses involved, and therefore only a complementary pair of literals are eliminated during each resolution step. As a consequence, the resulted clause has many literals, which affects the deduction efficiency. In this paper, a multi-clause synergized deduction algorithm is proposed based on contradiction separation rule. This algorithm allows multiple clauses used in deduction, and is able to eliminate more than one complementary pairs. The clause of contradiction separation is controllable and usually has less literals, which can effectively improve the inference ability. This multi-clause synergized algorithm adjusts the deduction order of clauses according to two kinds of weights, effective deduction weight and ineffective deduction weight. Backtracking mechanism is used to search for an optimal path, and effectively plan the deduction path. The algorithm is applied to the international top prover－Eprover 2.1, and Conference on Automated Deduction 2017 competition theorems (FOF division) are set as the test object. Eprover 2.1 with multi-clause synergized deduction algorithm outperformed Eprover 2.1 and solved 8 theorems more than Eprover 2.1. It also solved 31 theorems out of the 110 theorems unsolved by Eprover 2.1, accounting for 28.2% of the total.