Skip to main content
Top

1983 | OriginalPaper | Chapter

Refinement Theorems in Resolution Theory

Author : D. Luckham

Published in: Automation of Reasoning

Publisher: Springer Berlin Heidelberg

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

The paper discusses some basic refinements of the Resolution Principle which are intended to improve the speed and efficiency of theorem-proving programs based on this rule of inference. It is proved that two of the refinements preserve the logical complete­ness of the proof procedure when used separately, but not when used in conjunction. The results of some preliminary experiments with the refinements are given.

Metadata
Title
Refinement Theorems in Resolution Theory
Author
D. Luckham
Copyright Year
1983
Publisher
Springer Berlin Heidelberg
DOI
https://doi.org/10.1007/978-3-642-81955-1_27