Theory Resolution: Building in Nonequational Theories

Book One

Volume

Proceedings of the AAAI Conference on Artificial Intelligence, 3

Knowledge Representation and Problem Solving

Theory resolution constitutes a set of complete proce-dures 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 deci- sion 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 sys-tem.