---
title: "Designing Examples for Semantically Guided Hierarchical Deduction"
authors:
  - "Tie-Cheng Wang"
doi: ""
url: "https://ijcai.org/proceedings/1985/243"
pdf: "https://ijcai.org/proceedings/1985/0243.pdf"
venue: "Proceedings of the Ninth International Joint Conference on Artificial Intelligence"
year: 1985
pages: "1201-1206"
track: "Theorem Proving"
keywords:
---

# Designing Examples for Semantically Guided Hierarchical Deduction

Tie-Cheng Wang

*Proceedings of the Ninth International Joint Conference on Artificial Intelligence*, pages 1201-1206.

## Abstract

Sema.ntically guided hierarchical deduction prover is a resolution-based theorem-proving procedure which is capable of using the domain dependent knowledge presented in weil designed examples. This paper gives a.n overview of the basic deduction components of the prover, investigates some rules for human design of examples, and demonstrates their usage in proving several non-trivial theorems.