Designing Examples for Semantically Guided Hierarchical Deduction
Abstract
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.
Cite
Text
Wang. "Designing Examples for Semantically Guided Hierarchical Deduction." International Joint Conference on Artificial Intelligence, 1985.Markdown
[Wang. "Designing Examples for Semantically Guided Hierarchical Deduction." International Joint Conference on Artificial Intelligence, 1985.](https://mlanthology.org/ijcai/1985/wang1985ijcai-designing/)BibTeX
@inproceedings{wang1985ijcai-designing,
title = {{Designing Examples for Semantically Guided Hierarchical Deduction}},
author = {Wang, Tie-Cheng},
booktitle = {International Joint Conference on Artificial Intelligence},
year = {1985},
pages = {1201-1207},
url = {https://mlanthology.org/ijcai/1985/wang1985ijcai-designing/}
}