peter-2019.bib

@comment{{This file has been generated by bib2bib 1.99}}

@comment{{Command line: bib2bib -c 'year=2019 and not annote:"skip_html" and not annote:"unpublished"' -ob peter-2019.bib -oc peter-2019.cite peter.bib}}

@inproceedings{Baumgartner:Waldmann:hierarchic-superposition-reviewed:FP:2019,
  title = {Hierarchic Superposition Revisited},
  author = {Peter Baumgartner and Uwe Waldmann},
  booktitle = {Description Logic, Theory Combination, and All That},
  editor = {Carsten Lutz and Uli Sattler and Cesare Tinelli and Anni-Yasmin Turhan and Frank Wolter},
  year = {2019},
  publisher = {Springer},
  series = {LNCS},
  volume = {11560},
  pages = {15--56},
  url = {https://arxiv.org/abs/1904.03776},
  copyright = {Copyright Springer Verlag \url{http://www.springer.de/comp/lncs/index.html}},
  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
hierarchic superposition calculus of Bachmair, Ganzinger, and Waldmann
already supports such symbols, but, as we demonstrate, not optimally.
This paper aims to rectify the 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. We argue for the benefits of the resulting calculus and
provide two new completeness results: one for the fragment where all
background-sorted terms are ground and another one for a special
case of linear (integer or rational) arithmetic as a background theory.}
}

@misc{Baumgartner:Waldmann:hierarchic-superposition-reviewed:arxiv:2019,
  title = {Hierarchic Superposition Revisited},
  author = {Peter Baumgartner and Uwe Waldmann},
  year = {2019},
  journal = {CoRR},
  volume = {abs/1904.03776},
  url = {https://arxiv.org/abs/1904.03776},
  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
hierarchic superposition calculus of Bachmair, Ganzinger, and Waldmann
already supports such symbols, but, as we demonstrate, not optimally.
This paper aims to rectify the 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. We argue for the benefits of the resulting calculus and
provide two new completeness results: one for the fragment where all
background-sorted terms are ground and another one for a special
case of linear (integer or rational) arithmetic as a background theory.}
}