MPI-I-97-2-005
A theory of resolution
Bachmair, Leo and Ganzinger, Harald
May 1997, 79 pages.
.
Status: available - back from printing
We review the fundamental resolution-based methods for first-order
theorem proving and present them in a uniform
framework. We show that these calculi can
be viewed as specializations of non-clausal resolution with simplification.
Simplification techniques are justified with the help of a rather
general notion of redundancy for inferences.
As simplification and other techniques for the elimination of
redundancy are indispensable for an acceptable behaviour
of any practical theorem prover
this work is the first uniform treatment of resolution-like techniques
in which the avoidance of redundant computations attains the attention
it deserves.
In many cases our presentation of a resolution method will
indicate new ways of how to improve the method
over what was known previously.
We also give
answers to several open problems in the area.
Note:
To appear in J.A. Robinson, A. Voronkov (eds): Handbook of Automated Reasoning
Categories / Keywords:
Automated Aeduction, Resolution, Simplification
References to related material:
-
- Attachement: ATTQ9LM4 (616 KBytes)
URL to this document: https://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/1997-2-005
BibTeX
@TECHREPORT{BachmairGanzinger-97-mpii2-005,
AUTHOR = {Bachmair, Leo and Ganzinger, Harald},
TITLE = {A theory of resolution},
TYPE = {Research Report},
INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
ADDRESS = {Im Stadtwald, D-66123 Saarbr{\"u}cken, Germany},
NUMBER = {MPI-I-97-2-005},
MONTH = {May},
YEAR = {1997},
ISSN = {0946-011X},
NOTE = {To appear in J.A. Robinson, A. Voronkov (eds): Handbook of Automated Reasoning},
}