Skip to main content
CSIRO Logo Data 61 logo

Beagle — a hierarchic superposition theorem prover

Authors

Peter Baumgartner, Joshua Bax and Uwe Waldmann

NICTA

Max-Planck-Institute for Computer Science

Abstract

Beagle is an automated theorem prover for first-order logic modulo built-in theories. It implements a refined version of the hierarchic superposition calculus. This system description focuses on Beagle's proof procedure, background reasoning facilities, implementation, and experimental results.

BibTeX Entry

  @inproceedings{Baumgartner_BW_15,
    author           = {Baumgartner, Peter and Bax, Joshua and Waldmann, Uwe},
    month            = aug,
    year             = {2015},
    keywords         = {automated reasoning, first-order logic},
    address          = {Berlin, Germany},
    title            = {Beagle --- A Hierarchic Superposition Theorem Prover},
    pages            = {367--377},
    booktitle        = {International Conference on Automated Deduction},
    paperurl         = {https://ts.data61.csiro.au/publications/nicta_full_text/8726.pdf}
  }

Download