Help Privacy Policy Disclaimer
  Advanced SearchBrowse




Book Chapter

Resolution Theorem Proving


Bachmair,  Leo
Programming Logics, MPI for Informatics, Max Planck Society;


Ganzinger,  Harald
Programming Logics, MPI for Informatics, Max Planck Society;

External Resource
No external resources are shared
Fulltext (restricted access)
There are currently no full texts shared for your IP range.
Fulltext (public)
There are no public fulltexts stored in PuRe
Supplementary Material (public)
There is no public supplementary material available

Bachmair, L., & Ganzinger, H. (2001). Resolution Theorem Proving. In J. A. Robinson, & A. Voronkov (Eds.), Handbook of Automated Reasoning (pp. 19-99). Amsterdam, the Netherlands: Elsevier.

Cite as: https://hdl.handle.net/11858/00-001M-0000-000F-323F-9
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.