The consequence finding problem is a generalization of the refutation finding problem. The SOL-resolution which is a Model-Elimination-like calculus with Skip operation, is one of the most significant calculi for the consequence finding problem. The concept “completeness” of consequence-finding calculi differs from the one of refutation finding calculi, hence the pruning methods that are complete for refutation finding tasks may not be complete for consequence finding problems. In this paper, we first reformulate SOL-resolution within connection tableaux and properly strengthen a structural condition, called the skip-regularity, which reduces a great amount of the redundancies in the search space. Next we investigate various types of pruning methods, such as order-preserving reduction, lemma matching, merge, milt subsumption, etc, and show the completeness theorems of each pruning method for consequence finding. Finally we show Skip operation itself has a significantly important feature as a new local failure pruning method in consequence finding.
展开▼
