Look-ahead clause selection strategy for contradiction separation based automated deduction

摘要

Contradiction separation based dynamic automated deduction is a novel logic based automated deduction framework, which extends the static binary resolution inference rule to a dynamic multiple contradiction separation based automated deduction mechanism. The efficient implementation of this contradiction separation deduction lays, to a good extent, on how to select appropriate clauses and/or literals to construct the contradiction. This paper proposes a clause or literal selection strategy, so-called look-ahead strategy, which consider mainly the synergized effect of multi-clauses during the deduction process. Technical analysis along with some examples are provided to illustrate the feasibility of the proposed strategy.