Hierarchical deduction (Q1098332)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Hierarchical deduction |
scientific article |
Statements
Hierarchical deduction (English)
0 references
1987
0 references
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.
0 references
automated theorem proving
0 references
goal-oriented deduction
0 references
resolution unification
0 references
hierarchical deduction
0 references
0 references