English
 
User Manual Privacy Policy Disclaimer Contact us
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT

Released

Paper

Hierarchic Superposition Revisited

MPS-Authors
/persons/resource/persons45689

Waldmann,  Uwe
Automation of Logic, MPI for Informatics, Max Planck Society;

Locator
There are no locators available
Fulltext (public)

arXiv:1904.03776.pdf
(Preprint), 500KB

Supplementary Material (public)
There is no public supplementary material available
Citation

Baumgartner, P., & Waldmann, U. (2019). Hierarchic Superposition Revisited. Retrieved from http://arxiv.org/abs/1904.03776.


Cite as: http://hdl.handle.net/21.11116/0000-0004-03C0-F
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.