Abstract:
The aim of this talk is to extended Resolution Method by new rule, which simulate cut. We also will obtain upper and lower bounds on the complexity of refutation with and without this rule.
Key words and phrases:resolution method, refutation, cut, sequent, upper bound, lower bound.