Deutsch
 
Hilfe Datenschutzhinweis Impressum
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT
 
 
DownloadE-Mail
 Lokale TagsFreigabegeschichteDetailsÜbersicht
  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

 

einblenden: alle ausblenden: alle

Basisdaten

einblenden: ausblenden:
Datensatz-Permalink: https://hdl.handle.net/11858/00-001M-0000-000F-323F-9 Versions-Permalink: https://hdl.handle.net/11858/00-001M-0000-000F-3240-3
Genre: Buchkapitel

Dateien

einblenden: Dateien
ausblenden: Dateien
:
2001Handbook.ps.gz (beliebiger Volltext), 402KB
 
Datei-Permalink:
-
Name:
2001Handbook.ps.gz
Beschreibung:
-
OA-Status:
Sichtbarkeit:
Privat
MIME-Typ / Prüfsumme:
application/gzip
Technische Metadaten:
Copyright Datum:
-
Copyright Info:
This chapter appeared in the Handbook of Automated Reasoning, North Holland, 2001.
Lizenz:
-

Externe Referenzen

einblenden:

Urheber

einblenden:
ausblenden:
 Urheber:
Bachmair, Leo1, Autor           
Ganzinger, Harald1, Autor           
Affiliations:
1Programming Logics, MPI for Informatics, Max Planck Society, ou_40045              

Inhalt

einblenden:
ausblenden:
Schlagwörter: -
 Zusammenfassung: 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

einblenden:
ausblenden:
Sprache(n): eng - English
 Datum: 2010-03-122001
 Publikationsstatus: Erschienen
 Seiten: -
 Ort, Verlag, Ausgabe: Amsterdam, the Netherlands : Elsevier
 Inhaltsverzeichnis: -
 Art der Begutachtung: -
 Identifikatoren: eDoc: 519634
Anderer: Local-ID: C1256104005ECAFC-E89AFB3982578341C125648E00502FAC-BachmairGanzinger-01-har
 Art des Abschluß: -

Veranstaltung

einblenden:

Entscheidung

einblenden:

Projektinformation

einblenden:

Quelle 1

einblenden:
ausblenden:
Titel: Handbook of Automated Reasoning
Genre der Quelle: Buch
 Urheber:
Robinson, J. A., Herausgeber
Voronkov, A.1, Herausgeber           
Affiliations:
1 Programming Logics, MPI for Informatics, Max Planck Society, ou_40045            
Ort, Verlag, Ausgabe: Amsterdam, the Netherlands : Elsevier
Seiten: - Band / Heft: 1 Artikelnummer: - Start- / Endseite: 19 - 99 Identifikator: -