Trustworthy Systems

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

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