English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
  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

Files

show Files
hide Files
:
pwm.ps (Any fulltext), 111KB
 
File Permalink:
-
Name:
pwm.ps
Description:
-
OA-Status:
Visibility:
Private
MIME-Type / Checksum:
application/postscript
Technical Metadata:
Copyright Date:
-
Copyright Info:
-
License:
-

Locators

show

Creators

show
hide
 Creators:
Gaillourdet, Jean-Marie, Author
Hillenbrand, Thomas1, 2, 3, Author           
Löchner, Bernd3, Author           
Spies, Hendrik, Author
Baader, Franz3, Editor           
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              

Content

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

show
hide
Language(s): eng - English
 Dates: 2004-06-232003
 Publication Status: Issued
 Pages: -
 Publishing info: -
 Table of Contents: -
 Rev. Type: -
 Identifiers: eDoc: 201823
Other: Local-ID: C1256104005ECAFC-F7AE319E928299C3C1256D01002DD440-GaillourdetHillenbrandLoechner2003
 Degree: -

Event

show
hide
Title: CADE 2003
Place of Event: Miami, Florida
Start-/End Date: 2003-07-28 - 2003-08-02

Legal Case

show

Project information

show

Source 1

show
hide
Title: Automated deduction, CADE-19 : 19th International Conference on Automated Deduction
Source Genre: Proceedings
 Creator(s):
Affiliations:
Publ. Info: Berlin, Germany : Springer
Pages: - Volume / Issue: - Sequence Number: - Start / End Page: 317 - 321 Identifier: -

Source 2

show
hide
Title: Lecture Notes in Artificial Intelligence
Source Genre: Series
 Creator(s):
Affiliations:
Publ. Info: -
Pages: - Volume / Issue: 2741 Sequence Number: - Start / End Page: - Identifier: -