Skip to main content

TS

Hierarchic superposition with weak abstraction and the beagle theorem prover

Authors

Peter Baumgartner and Uwe Waldmann

NICTA

Max-Planck-Institute for Computer Science

Abstract

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

  @inproceedings{Baumgartner_Waldmann_14,
    author           = {Baumgartner, Peter and Waldmann, Uwe},
    month            = feb,
    slides           = {http://ts.data61.csiro.au/publications/nicta_slides/7905.pdf},
    year             = {2014},
    keywords         = {automated reasoning, first-order logic},
    title            = {Hierarchic superposition with weak abstraction and the Beagle theorem prover},
    booktitle        = {Deduction and Arithmetic (Dagstuhl Seminar 13411)},
    pages            = {7},
    address          = {Dagstuhl, Germany,}
  }

Download

Served by Apache on Linux on seL4.