Deutsch
 
Hilfe Datenschutzhinweis Impressum
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT
Zur Ablage hinzufügen
 Lokale TagsFreigabegeschichteDetailsÜbersicht
  The New WALDMEISTER Loop at Work

Gaillourdet, J.-M., Hillenbrand, T., Löchner, B., & Spies, H. (2003). The New WALDMEISTER Loop at Work. In Automated deduction, CADE-19: 19th International Conference on Automated Deduction (pp. 317-321). Berlin, Germany: Springer.

Item is

 

einblenden: alle ausblenden: alle

Basisdaten

einblenden: ausblenden:
Datensatz-Permalink: https://hdl.handle.net/11858/00-001M-0000-000F-2E5A-7 Versions-Permalink: https://hdl.handle.net/11858/00-001M-0000-000F-2E5D-1
Genre: Konferenzbeitrag

Dateien

einblenden: Dateien
ausblenden: Dateien
:
pwm.ps (beliebiger Volltext), 111KB
 
Datei-Permalink:
-
Name:
pwm.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:
Gaillourdet, Jean-Marie, Autor
Hillenbrand, Thomas1, 2, 3, Autor           
Löchner, Bernd3, Autor           
Spies, Hendrik, Autor
Baader, Franz3, Herausgeber           
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: We present recent developments within the theorem prover \textsc{Waldmeister}. They rely on a novel organization of the underlying saturation-based proof procedure into a system architecture. As is known, the saturation process tends to quickly fill the memory available unless preventive measures are employed. To overcome this problem, our new ``\textsc{Waldmeister} loop'' features a highly compact representation of the search state, exploiting its inherent structure. The implementation just being available, the cost and the benefits of the concept now can exactly be measured. Indeed are our expectations met concerning the drastic cut-down of memory usage with only moderate overhead of time. In addition it has turned out that the revealed structure of the search state paves the way to an easily implemented parallelization of the prover with modest communication requirements and rewarding speed-ups. In order to minimize communication-related latencies, we discuss some variations of the loop to maximally profit from multiple processors.

Details

einblenden:
ausblenden:
Sprache(n): eng - English
 Datum: 2004-06-232003
 Publikationsstatus: Erschienen
 Seiten: -
 Ort, Verlag, Ausgabe: -
 Inhaltsverzeichnis: -
 Art der Begutachtung: -
 Identifikatoren: eDoc: 201823
Anderer: Local-ID: C1256104005ECAFC-F7AE319E928299C3C1256D01002DD440-GaillourdetHillenbrandLoechner2003
 Art des Abschluß: -

Veranstaltung

einblenden:
ausblenden:
Titel: CADE 2003
Veranstaltungsort: Miami, Florida
Start-/Enddatum: 2003-07-28 - 2003-08-02

Entscheidung

einblenden:

Projektinformation

einblenden:

Quelle 1

einblenden:
ausblenden:
Titel: Automated deduction, CADE-19 : 19th International Conference on Automated Deduction
Genre der Quelle: Konferenzband
 Urheber:
Affiliations:
Ort, Verlag, Ausgabe: Berlin, Germany : Springer
Seiten: - Band / Heft: - Artikelnummer: - Start- / Endseite: 317 - 321 Identifikator: -

Quelle 2

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