| Abstract: | In 1994,
Bachmair, Ganzinger, and Waldmann introduced the hierarchical
superposition calculus as a generalization of the superposition
calculus for black-box style theory reasoning.
Their calculus works in a framework of hierarchic specifications.
It tries to prove the
unsatisfiability of a set of clauses with respect to interpretations
that extend a background model such as the integers with linear arithmetic
conservatively, that is, without
identifying distinct elements of old sorts ("confusion") and without
adding new elements to old sorts ("junk").
We show how the calculus can be improved,
report on practical experiments,
and present a new completeness result for
non-compact classes of background models
(i.e., linear integer or rational arithmetic restricted to
standard models). |
