Hierarchic Superposition Revisited

Peter Baumgartner 1 Uwe Waldmann 2, 3
3 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
MPII - Max-Planck-Institut für Informatik, Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
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.
Document type :
Book sections
Complete list of metadatas

Cited literature [30 references]  Display  Hide  Download

https://hal.inria.fr/hal-02402941
Contributor : Stephan Merz <>
Submitted on : Tuesday, December 10, 2019 - 4:35:14 PM
Last modification on : Tuesday, December 17, 2019 - 2:25:38 AM

File

BaumgartnerWaldmann2019FB-auth...
Files produced by the author(s)

Identifiers

Collections

Citation

Peter Baumgartner, Uwe Waldmann. Hierarchic Superposition Revisited. Carsten Lutz and Uli Sattler and Cesare Tinelli and Anni-Yasmin Turhan and Frank Wolter. Description Logic, Theory Combination, and All That - Essays Dedicated to Franz Baader on the Occasion of His 60th Birthday, 11560, Springer, pp.15-56, 2019, Lecture Notes in Computer Science, ⟨10.1007/978-3-030-22102-7_2⟩. ⟨hal-02402941⟩

Share

Metrics

Record views

25

Files downloads

30