hide
Free keywords:
-
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 a new completeness result for the fragment where
all background-sorted terms are ground.
