@INPROCEEDINGS{AlthausEtAlFrocos2009,
AUTHOR = {Althaus, Ernst and Kruglov, Evgeny and Weidenbach, Christoph},
EDITOR = {Ghilardi, Silvio and Sebastiani, Roberto},
TITLE = {Superposition Modulo Linear Arithmetic SUP(LA)},
BOOKTITLE = {7th international Symposium on Frontiers of Combining Systems (FroCos 2009)},
PUBLISHER = {Springer},
YEAR = {2009},
VOLUME = {5749},
PAGES = {84--99},
SERIES = {Lecture Notes in Artificial Intelligence},
ADDRESS = {Trento, Italy},
MONTH = {September},
subproject={S2},
access={open},
bibtex={althaus.frocos2009.bib},
pdf={althaus.frocos2009.pdf},
abstract={The hierarchical superposition based theorem proving calculus
of Bachmair, Ganzinger, and Waldmann enables the hierarchic
combination of a theory with full first-order logic. If a clause set of the
combination enjoys a sufficient completeness criterion, the calculus is
even complete. We instantiate the calculus for the theory of linear arithmetic.
In particular, we develop new effective versions for the standard
superposition redundancy criteria taking the linear arithmetic theory
into account. The resulting calculus is implemented in SPASS(LA) and
extends the state of the art in proving properties of first-order formulas
over linear arithmetic.},
}