Hierarchical deduction (Q1098332)

The main contribution of the paper is the goal-oriented hierarchical deduction proof procedure. The procedure proves a theorem by producing not just one but all the acceptable resolvents from the goal clause. There is a set of completeness-preserving refinements to constrain the generation of the irrelevant resolvents. The paper describes a ground hierarchical deduction procedure applicable to propositional logic and then extends this procedure for first-order logic. A semantically guided hierarchical deduction and a partial set of support strategies are defined as two methods to reduce the search space. The implementation results are included. The authors give an outline of the implemented procedure (HD-Prover) and a list of automatically proved theorems.