Automated deduction by theory resolution
type: Item
instance of: scholarly article
title: Automated deduction by theory resolution
zbMATH Open document ID: 0616.68076
DOI: 10.1007/BF00244275
author: Mark E. Stickel
published in: Journal of Automated Reasoning
publication date: 1985-01-01T00:00:00Z
review text: Theory resolution constitutes a set of complete procedures for incorporating theories into a resolution theorem-proving program, thereby making it unnecessary to resolve directly upon axioms of the theory. This can reduce the length of proofs and the size of the search space. Theory resolution effects a beneficial division of labor, improving the performance of the theorem prover and increasing the applicability of the specialized reasoning procedures. Total theory resolution utilizes a decision procedure that is capable of determining unsatisfiability of any set of clauses using predicates in the theory. Partial theory resolution employs a weaker decision procedure that can determine potential unsatisfiability of sets of literals. Applications include the building in of both mathematical and special decision procedures, e.g., for the taxonomic information furnished by a knowledge representation system. Theory resolution is a generalization of numerous previously known resolution refinements. Its power is demonstrated by comparing solutions of 'Schubert's Steamroller' challenge problem with and without building in axioms through theory resolution.
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 3999323
zbMATH Keywords: decision procedures
zbMATH Keywords: resolution theorem-proving
MaRDI profile type: Publication
full work available at URL: https://doi.org/10.1007/bf00244275
OpenAlex ID: W2047669821
description: scientific article; zbMATH DE number 3999323