Max-Planck-Institut für Informatik
max planck institut
informatik
mpii logo Minerva of the Max Planck Society
 

MPI-I-97-2-005

A theory of resolution

Bachmair, Leo and Ganzinger, Harald

MPI-I-97-2-005. May 1997, 79 pages. | Status: available - back from printing | Next --> Entry | Previous <-- Entry

Abstract in LaTeX format:
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
Acknowledgement:
Categories / Keywords: Automated Aeduction, Resolution, Simplification
References to related material:
http://www.mpi-sb.mpg.de/\~{}hg/pra.html\#MPI-I-97-2-005

To download this research report, please select the type of document that fits best your needs.Attachement Size(s):
MPI-I-97-2-005.ps616 KBytes
Please note: If you don't have a viewer for PostScript on your platform, try to install GhostScript and GhostView

URL to this document: http://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/1997-2-005

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