Deutsch
 
Hilfe Datenschutzhinweis Impressum
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT
Zur Ablage hinzufügen
 Lokale TagsFreigabegeschichteDetailsÜbersicht
  The Next WALDMEISTER Loop

Hillenbrand, T., & Löchner, B. (2002). The Next WALDMEISTER Loop. In A. Voronkov (Ed.), Automated deduction, CADE-18: 18th International Conference on Automated Deduction (pp. 486-500). Heidelberg, Germany: Springer.

Item is

 

einblenden: alle ausblenden: alle

Basisdaten

einblenden: ausblenden:
Datensatz-Permalink: https://hdl.handle.net/11858/00-001M-0000-000F-30F6-A Versions-Permalink: https://hdl.handle.net/11858/00-001M-0000-000F-30F9-4
Genre: Konferenzbeitrag

Dateien

einblenden: Dateien
ausblenden: Dateien
:
wmloop.ps (beliebiger Volltext), 386KB
 
Datei-Permalink:
-
Name:
wmloop.ps
Beschreibung:
-
OA-Status:
Sichtbarkeit:
Privat
MIME-Typ / Prüfsumme:
application/postscript
Technische Metadaten:
Copyright Datum:
-
Copyright Info:
-
Lizenz:
-

Externe Referenzen

einblenden:

Urheber

einblenden:
ausblenden:
 Urheber:
Hillenbrand, Thomas1, 2, 3, Autor           
Löchner, Bernd3, Autor           
Affiliations:
1International Max Planck Research School, MPI for Informatics, Max Planck Society, ou_1116551              
2Automation of Logic, MPI for Informatics, Max Planck Society, ou_1116545              
3Programming Logics, MPI for Informatics, Max Planck Society, ou_40045              

Inhalt

einblenden:
ausblenden:
Schlagwörter: -
 Zusammenfassung: In saturation-based theorem provers, the reasoning process consists in constructing the closure of an axiom set under inferences. As is well-known, this process tends to quickly fill the memory available unless preventive measures are employed. For implementations based on the DISCOUNT loop, the passive facts are responsible for most of the memory consumption. We present a refinement of that loop allowing such a compression that the space needed for the passive facts is linearly bound by the number of active facts. In practice, this will reduce memory consumption in the WALDMEISTER system by more than one order of magnitude as compared to previous compression schemes.

Details

einblenden:
ausblenden:
Sprache(n): eng - English
 Datum: 2007-03-202002
 Publikationsstatus: Erschienen
 Seiten: -
 Ort, Verlag, Ausgabe: -
 Inhaltsverzeichnis: -
 Art der Begutachtung: -
 Identifikatoren: eDoc: 521707
Anderer: Local-ID: C125716C0050FB51-4D570162B4332D6DC12572A400330506-HL02-CADE18
 Art des Abschluß: -

Veranstaltung

einblenden:
ausblenden:
Titel: CADE 2002
Veranstaltungsort: Copenhagen, Denmark
Start-/Enddatum: 2002-07-27 - 2002-07-30

Entscheidung

einblenden:

Projektinformation

einblenden:

Quelle 1

einblenden:
ausblenden:
Titel: Automated deduction, CADE-18 : 18th International Conference on Automated Deduction
Genre der Quelle: Konferenzband
 Urheber:
Voronkov, Andrei1, Herausgeber           
Affiliations:
1 Programming Logics, MPI for Informatics, Max Planck Society, ou_40045            
Ort, Verlag, Ausgabe: Heidelberg, Germany : Springer
Seiten: - Band / Heft: - Artikelnummer: - Start- / Endseite: 486 - 500 Identifikator: ISBN: 3-540-43931-5

Quelle 2

einblenden:
ausblenden:
Titel: Lecture Notes in Artificial Intelligence
Genre der Quelle: Reihe
 Urheber:
Affiliations:
Ort, Verlag, Ausgabe: -
Seiten: - Band / Heft: 2392 Artikelnummer: - Start- / Endseite: - Identifikator: -