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
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:
|To download this research report, please select the type of document that fits best your needs.||Attachement Size(s):|
|Please note: If you don't have a viewer for PostScript on your platform, try to install GhostScript and GhostView|