Skip to main content

TS

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},
    title            = {Beagle - A Hierarchic Superposition Theorem Prover},
    booktitle        = {International Conference on Automated Deduction},
    pages            = {367-377},
    address          = {Berlin, Germany}
  }

Download