Skip to main content

Hierarchic superposition with weak abstraction and the beagle theorem prover


Peter Baumgartner and Uwe Waldmann


Max-Planck-Institute for Computer Science


Many applications of automated deduction require reasoning in first-order logic modulo background theories, in particular some form of integer arithmetic. A major unsolved research challenge is to design theorem provers that are "reasonably complete" even in the presence of free function symbols ranging into a background theory sort. The earlier hierarchic superposition calculus of Bachmair, Ganzinger, and Waldmann already supports such symbols, but, not optimally. We have devised a new calculus, hierarchic superposition with weak abstraction, which rectifies this situation by introducing a novel form of clause abstraction, a core component in the hierarchic superposition calculus for transforming clauses into a form needed for internal operation. Additionally, it includes a definition rule that is generally useful to find refutations more often, and, specifically, gives completeness for the clause logic fragment where all background-sorted terms are ground. The talk provides an overview of the calculus, its implementation in the Beagle theorem prover and experiments with it.

BibTeX Entry

    month            = feb,
    keywords         = {automated reasoning, first-order logic},
    paperurl         = {},
    booktitle        = {Deduction and Arithmetic (Dagstuhl Seminar 13411)},
    slides           = {},
    author           = {Baumgartner, Peter and Waldmann, Uwe},
    year             = {2014},
    pages            = {7},
    title            = {Hierarchic superposition with weak abstraction and the Beagle theorem prover},
    address          = {Dagstuhl, Germany,}