Help Privacy Policy Disclaimer
  Advanced SearchBrowse





Hierarchic Superposition Revisited


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

External Resource
No external resources are shared
Fulltext (restricted access)
There are currently no full texts shared for your IP range.
Fulltext (public)

(Preprint), 500KB

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

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

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