Skip to main content


Beagle - a hierarchic superposition theorem prover


Peter Baumgartner, Joshua Bax and Uwe Waldmann


Max-Planck-Institute for Computer Science


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

    author           = {Baumgartner, Peter and Bax, Joshua and Waldmann, Uwe},
    month            = aug,
    year             = {2015},
    keywords         = {automated reasoning, first-order logic},
    title            = {Beagle - A Hierarchic Superposition Theorem Prover},
    booktitle        = {International Conference on Automated Deduction},
    pages            = {367-377},
    address          = {Berlin, Germany}


Served by Apache on Linux on seL4.
Served by Apache on Linux on seL4.