A note on the analysis of theorem-proving strategies
Maria Paola Bonacina · 1996
In recent work David Plaisted proposed an approach to analyze the search efficiency of theorem-proving strategies, and applied it to Horn propositional logic. In this note we comment on this approach. We point out a number of problematic issues in the modelling of search and the analysis of strategies, including the formalization of the search plan, the representation of contraction, and the duality of forward and backward reasoning. These issues are especially relevant for the analysis of strategies in first-order logic, where the search space is infinite.