English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
Add to Basket
 Local TagsRelease HistoryDetailsSummary
  Resolution Theorem Proving

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.

Item is

 

show all hide all

Basic

show hide
Item Permalink: https://hdl.handle.net/11858/00-001M-0000-000F-323F-9 Version Permalink: https://hdl.handle.net/11858/00-001M-0000-000F-3240-3
Genre: Book Chapter

Files

show Files
hide Files
:
2001Handbook.ps.gz (Any fulltext), 402KB
 
File Permalink:
-
Name:
2001Handbook.ps.gz
Description:
-
OA-Status:
Visibility:
Private
MIME-Type / Checksum:
application/gzip
Technical Metadata:
Copyright Date:
-
Copyright Info:
This chapter appeared in the Handbook of Automated Reasoning, North Holland, 2001.
License:
-

Locators

show

Creators

show
hide
 Creators:
Bachmair, Leo1, Author           
Ganzinger, Harald1, Author           
Affiliations:
1Programming Logics, MPI for Informatics, Max Planck Society, ou_40045              

Content

show
hide
Free keywords: -
 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.

Details

show
hide
Language(s): eng - English
 Dates: 2010-03-122001
 Publication Status: Issued
 Pages: -
 Publishing info: Amsterdam, the Netherlands : Elsevier
 Table of Contents: -
 Rev. Type: -
 Identifiers: eDoc: 519634
Other: Local-ID: C1256104005ECAFC-E89AFB3982578341C125648E00502FAC-BachmairGanzinger-01-har
 Degree: -

Event

show

Legal Case

show

Project information

show

Source 1

show
hide
Title: Handbook of Automated Reasoning
Source Genre: Book
 Creator(s):
Robinson, J. A., Editor
Voronkov, A.1, Editor           
Affiliations:
1 Programming Logics, MPI for Informatics, Max Planck Society, ou_40045            
Publ. Info: Amsterdam, the Netherlands : Elsevier
Pages: - Volume / Issue: 1 Sequence Number: - Start / End Page: 19 - 99 Identifier: -