WALDMEISTER - High-Performance Equational Deduction

Waldmeister is a high-performance theorem prover for unit equational first-order logic. In the making of Waldmeister, we have applied an engineering approach, identifying the critical points with respect to efficiency in time and space. Our logical three-level system model consists of the basic oper...

Full description

Saved in:
Bibliographic Details
Published in:Journal of automated reasoning 1997-04, Vol.18 (2), p.265
Main Authors: Hillenbrand, Thomas, Buch, Arnim, Vogt, Roland, Löchner, Bernd
Format: Article
Language:English
Subjects:
Algorithms
Studies
Citations: Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Waldmeister is a high-performance theorem prover for unit equational first-order logic. In the making of Waldmeister, we have applied an engineering approach, identifying the critical points with respect to efficiency in time and space. Our logical three-level system model consists of the basic operations on the lowest level, where we put great stress on efficient data structures and algorithms. For the middle level, where the inference steps are aggregated into an inference machine, flexible adjustment has proven essential during experimental evaluation. The top level holds control strategy and reduction ordering. Although at this level only standard strategies are employed, really large proof tasks have been managed in reasonable time.[PUBLICATION ABSTRACT]
ISSN:0168-7433
1573-0670
DOI:10.1023/A:1005872405899