# Hierarchic superposition with weak abstraction and the beagle theorem prover

## Authors

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,} }