Hierarchical deduction

DOI10.1007/BF00381144zbMath0636.68120OpenAlexW2913781829MaRDI QIDQ1098332

Tie-Cheng Wang, W. W. Bledsoe

Publication date: 1987

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf00381144

zbMATH Keywords

automated theorem provinggoal-oriented deductionhierarchical deductionresolution unification

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items

Conditional term rewriting and first-order theorem proving, A semantic backward chaining proof system, Refinements to depth-first iterative-deepening search in automatic theorem proving, Semantically guided first-order theorem proving using hyper-linking, Combining logical and algebraic techniques for natural style proving in elementary analysis, A typed resolution principle for deduction with conditional typing theory

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Non-resolution theorem proving
• Linear resolution with selection function
• Problems and Experiments for and with Automated Theorem-Proving Programs
• An Implementation of the Model Elimination Proof Procedure
• A New Class of Automated Theorem-Proving Algorithms
• Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
• Mechanical Theorem-Proving by Model Elimination
• A Simplified Format for the Model Elimination Theorem-Proving Procedure
• A Linear Format for Resolution With Merging and a New Technique for Establishing Completeness