MPI-INF/SWS Research Reports 1991-2021

2. Number - All Departments


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.
To appear in J.A. Robinson, A. Voronkov (eds): Handbook of Automated Reasoning
Categories / Keywords:
Automated Aeduction, Resolution, Simplification
References to related material:\~{}hg/pra.html\#MPI-I-97-2-005

  • Attachement: ATTQ9LM4 (616 KBytes)

URL to this document:

Hide details for BibTeXBibTeX
  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},