Acknowledgements

De-partment of Broadband, Communications and the Digital Economy and the Australian Research Council through the ICT Centre of Excellence program. We would like to thank the anonymous reviewers of CADE-24 for their helpful comments. Many applications of automated deduction require reasoning in first-order logic modulo background theories, in particular some form of integer arith-metic. A major unsolved research challenge is to design theorem provers that are “reasonably complete ” even in the presence of free function symbols rang-ing 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