Hierarchical deduction
type: Item
instance of: scholarly article
title: Hierarchical deduction
zbMATH Open document ID: 0636.68120
DOI: 10.1007/BF00381144
author: Tie-Cheng Wang
author: W. W. Bledsoe
published in: Journal of Automated Reasoning
publication date: 1987-01-01T00:00:00Z
review text: 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.
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 03B35
zbMATH DE Number: 4037273
zbMATH Keywords: automated theorem proving
zbMATH Keywords: goal-oriented deduction
zbMATH Keywords: resolution unification
zbMATH Keywords: hierarchical deduction
MaRDI profile type: Publication
cites work: A Linear Format for Resolution With Merging and a New Technique for Establishing Completeness
cites work: Non-resolution theorem proving
cites work: Q3880319
cites work: Q5679729
cites work: Linear resolution with selection function
cites work: Mechanical Theorem-Proving by Model Elimination
cites work: A Simplified Format for the Model Elimination Theorem-Proving Procedure
cites work: An Implementation of the Model Elimination Proof Procedure
cites work: Q4139711
cites work: Problems and Experiments for and with Automated Theorem-Proving Programs
cites work: A New Class of Automated Theorem-Proving Algorithms
cites work: Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
full work available at URL: https://doi.org/10.1007/bf00381144
OpenAlex ID: W2913781829
Recommended article: Hierarchical logical consequence
Recommended article: Hierarchies in Dependence Logic
Recommended article: Hierarchical propositions
Recommended article: Hierarchical Argumentation
Recommended article: On hierarchical propositions
Recommended article: Automated Deduction – CADE-20
Recommended article: Hierarchical hybrid logic
Recommended article: Hierarchies in independence logic
Recommended article: Q4697038
Recommended article: Q4235216
description: scientific article; zbMATH DE number 4037273