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.
CITATION STYLE
Hillenbrand, T., & Löchner, B. (2002). The next WALDMEISTER loop. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2392, pp. 486–500). Springer Verlag. https://doi.org/10.1007/3-540-45620-1_38
Mendeley helps you to discover research relevant for your work.