Designing examples for semantically guided hierarchical deduction
Tie Cheng Wang · International Joint Conference on Artificial Intelligence · 1985
Semantically guided hierarchical deduction prover is a resolution-based theorem-proving procedure which is capable of using the domain dependent knowledge presented in well designed examples. This paper gives an 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.