A new subsumption method in the connection graph proof procedure

AbstractCompared to most of the other resolution-based proof procedures, the connection graph proof procedure (CGPP) is superior due to its effective search space reduction rules. A test for subsumption in CGPP is sufficiently efficient in comparison with the standard test. But the subsumption with no restriction may cause logical inconsistency. The restriction on subsumption to maintain the consistency has been an open problem since it was first noticed in 1981. We define a newθ-subsumption which maintains the logical consistency and provides the graph transformation method which makes C subsume D with the new definition if C subsumes D with the original definition ofθ-sumsumption.In the subsumption test in CGPP, it is essential to find a set of pairwise strongly compatible matching substitutions between literals in two clauses. This paper presents an algorithm which finds a set of pairwise strongly compatible matching substitutions efficiently, based on both the reduction of possible matching substitutions and bit operations. The worst-case time complexity of this algorithm is analyzed in terms of the estimated maximal number of string comparisons and it is shown that our complexity is lower than the other algorithms based on the s-link test.Based on the new definition of subsumption and the improved algorithm for the pairwise strongly compatible test, an unrestricted subsumption algorithm and a restricted subsumption algorithm are suggested