Part, Chapter of a Book
@InBook, Buchkapitel
Beitrag im Sammelband


Show entries of:

this year (2024) | last year (2023) | two years ago (2022) | Notes URL

Action:

login to update
Options:








Author, Editor
Author(s):
Bachmair, Leo
Ganzinger, Harald		dblp
dblp
Editor(s):
Robinson, J. A.
Voronkov, A.		dblp
dblp

BibTeX cite key*:

BachmairGanzinger-01-har

Title, Booktitle

Title*:

Resolution Theorem Proving


2001Handbook.ps.gz (401.43 KB)

Booktitle*:

Handbook of Automated Reasoning

Chapter:

2

Series:


Language:

English

Publisher

Name*:

Elsevier
URL:

http://www.elsevier.com/

Address*:

Amsterdam, the Netherlands
Publication Type:


Vol, No, pp., Year

Volume:

1
Number:


Edition:


Pages*:

19-99

Month:


VG Wort Pages:


ISBN:


Year*:

2001

Abstract, Links, ©

Note:


LaTeX Abstract:

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.

URL Abstract:


Tags, Keywords:


Copyright Message:

This chapter appeared in the Handbook of Automated Reasoning, North Holland, 2001.

HyperLinks / References / URLs:

http://www.elsevier.nl/locate/isbn/0444829490
http://www.cs.man.ac.uk/~voronkov/handbook-ar/index.html

Personal Comments:


Download
Access Level:


Correlation
MPG Unit:
Max-Planck-Institut für Informatik
MPG Subunit:
Programming Logics Group
Audience:
experts only
Appearance:
MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat, CCL bibliography, VG Wort
BibTeX Entry:
@INBOOK{BachmairGanzinger-01-har,
AUTHOR = {Bachmair, Leo and Ganzinger, Harald},
 EDITOR = {Robinson, J. A. and Voronkov, A.},
 TITLE = {Resolution Theorem Proving},
 BOOKTITLE = {Handbook of Automated Reasoning},
 PUBLISHER = {Elsevier},
 YEAR = {2001},
 VOLUME = {1},
 CHAPTER = {2},
 PAGES = {19--99},
 ADDRESS = {Amsterdam, the Netherlands},
}

Entry last modified by Harald Ganzinger, 03/12/2010
Show details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)
Hide details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)

Editor(s)
Harald Ganzinger		Created
05/05/1997 04:35:50 PM
Revisions
25.
24.
23.
22.
21.		Editor(s)
Harald Ganzinger
Uwe Brahm
Uwe Brahm
Christine Kiesel
Christine Kiesel		Edit Dates
16.05.2003 10:16:23
07.04.2002 19:26:35
03/27/2002 10:10:13 PM
17.01.2002 17:17:41
29.08.2001 13:40:20