Efficient proofs in propositional calculus with inverse resolution

The main problem in using resolution to prove the validity of propositional formulas is inefficiency, because the search is essentially blind. Inversion of the resolution principle seems to lead to efficient and guided proofs if compared with classical resolution-based strategies. To estimate the maximum complexity of the inverse resolution strategy, it has been implemented in the inverse resolution algorithm (IRA), which is a breadth-first visiting algorithm of a graph built with the clauses of the given set; every vertex is labeled with a clause, and for every pair of complementary literals there exists an arc joining the two vertexes labeled with the clauses they belong to. The inverse resolution strategy is complete and strongly more efficient than classical strategies based on resolution.<>