Theory Resolution: Building in Nonequational Theories
Abstract
Theory resolution constitutes a set of complete procedures for building nonequational theories into a resolution theorem-proving program so that axioms of the theory need never be resolved upon. Total theory resolution uses a decision procedure that is capable of determining inconsistency of any set of clauses using predicates in the theory. Partial theory resolution employs a weaker decision procedure that can determine potential inconsistency of a pair of literals. Applications include the building in of both mathematical and special decision procedures, such as for the taxonomic information furnished by a knowledge representation system.
Cite
Text
Stickel. "Theory Resolution: Building in Nonequational Theories." AAAI Conference on Artificial Intelligence, 1983.Markdown
[Stickel. "Theory Resolution: Building in Nonequational Theories." AAAI Conference on Artificial Intelligence, 1983.](https://mlanthology.org/aaai/1983/stickel1983aaai-theory/)BibTeX
@inproceedings{stickel1983aaai-theory,
title = {{Theory Resolution: Building in Nonequational Theories}},
author = {Stickel, Mark E.},
booktitle = {AAAI Conference on Artificial Intelligence},
year = {1983},
pages = {391-397},
url = {https://mlanthology.org/aaai/1983/stickel1983aaai-theory/}
}