de.mpg.escidoc.pubman.appbase.FacesBean
Deutsch
 
Hilfe Wegweiser Datenschutzhinweis Impressum Kontakt
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT

Freigegeben

Konferenzbeitrag

The Next WALDMEISTER Loop

MPG-Autoren
http://pubman.mpdl.mpg.de/cone/persons/resource/persons44621

Hillenbrand,  Thomas
International Max Planck Research School, MPI for Informatics, Max Planck Society;
Automation of Logic, MPI for Informatics, Max Planck Society;
Programming Logics, MPI for Informatics, Max Planck Society;

http://pubman.mpdl.mpg.de/cone/persons/resource/persons44934

Löchner,  Bernd
Programming Logics, MPI for Informatics, Max Planck Society;

Externe Ressourcen
Es sind keine Externen Ressourcen verfügbar
Volltexte (frei zugänglich)
Es sind keine frei zugänglichen Volltexte verfügbar
Ergänzendes Material (frei zugänglich)
Es sind keine frei zugänglichen Ergänzenden Materialien verfügbar
Zitation

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.


Zitierlink: http://hdl.handle.net/11858/00-001M-0000-000F-30F6-A
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.