WALDMEISTER - High-Performance Equational Deduction

WALDMEISTER - High-Performance Equational Deduction. Hillenbrand, T., Buch, A., Vogt, R., & Löchner, B. Journal of Automated Reasoning, 18(2):265--270, 1997.

Paper doi abstract bibtex

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.

@article{hillenbrand1997,
abstract = {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.},
author = {Hillenbrand, Thomas and Buch, Arnim and Vogt, Roland and L{\"{o}}chner, Bernd},
doi = {10.1023/A:1005872405899},
issn = {1573-0670},
journal = {Journal of Automated Reasoning},
number = {2},
pages = {265--270},
title = {{WALDMEISTER - High-Performance Equational Deduction}},
url = {https://doi.org/10.1023/A:1005872405899},
volume = {18},
year = {1997}
}

Downloads: 0

{"_id":"Pmxn7zCZ9pznGnbWa","bibbaseid":"hillenbrand-buch-vogt-lchner-waldmeisterhighperformanceequationaldeduction-1997","downloads":0,"creationDate":"2017-09-01T03:35:40.584Z","title":"WALDMEISTER - High-Performance Equational Deduction","author_short":["Hillenbrand, T.","Buch, A.","Vogt, R.","Löchner, B."],"year":1997,"bibtype":"article","biburl":"https://raw.githubusercontent.com/jonaprieto/athena/master/paper/ref.bib","bibdata":{"bibtype":"article","type":"article","abstract":"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.","author":[{"propositions":[],"lastnames":["Hillenbrand"],"firstnames":["Thomas"],"suffixes":[]},{"propositions":[],"lastnames":["Buch"],"firstnames":["Arnim"],"suffixes":[]},{"propositions":[],"lastnames":["Vogt"],"firstnames":["Roland"],"suffixes":[]},{"propositions":[],"lastnames":["Löchner"],"firstnames":["Bernd"],"suffixes":[]}],"doi":"10.1023/A:1005872405899","issn":"1573-0670","journal":"Journal of Automated Reasoning","number":"2","pages":"265--270","title":"WALDMEISTER - High-Performance Equational Deduction","url":"https://doi.org/10.1023/A:1005872405899","volume":"18","year":"1997","bibtex":"@article{hillenbrand1997,\nabstract = {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.},\nauthor = {Hillenbrand, Thomas and Buch, Arnim and Vogt, Roland and L{\\\"{o}}chner, Bernd},\ndoi = {10.1023/A:1005872405899},\nissn = {1573-0670},\njournal = {Journal of Automated Reasoning},\nnumber = {2},\npages = {265--270},\ntitle = {{WALDMEISTER - High-Performance Equational Deduction}},\nurl = {https://doi.org/10.1023/A:1005872405899},\nvolume = {18},\nyear = {1997}\n}\n","author_short":["Hillenbrand, T.","Buch, A.","Vogt, R.","Löchner, B."],"key":"hillenbrand1997","id":"hillenbrand1997","bibbaseid":"hillenbrand-buch-vogt-lchner-waldmeisterhighperformanceequationaldeduction-1997","role":"author","urls":{"Paper":"https://doi.org/10.1023/A:1005872405899"},"downloads":0},"search_terms":["waldmeister","high","performance","equational","deduction","hillenbrand","buch","vogt","löchner"],"keywords":[],"authorIDs":[],"dataSources":["8jafqMAWgB7XP4FTZ"]}