Hierarchic superposition revisited

DOI10.1007/978-3-030-22102-7_2MaRDI QIDQ2185457zbMATH OpenOpenAlexFDO

Authors Peter Baumgartner, Uwe Waldmann

Publication date 4 June 2020

Full work available at URL https://arxiv.org/abs/1904.03776

zbMATH Keywords

automated deductioncombinations of theoriessuperposition calculus

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

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.

Recommendations

• Hierarchic superposition with weak abstraction
• scientific article; zbMATH DE number 1300967
• Superposition modulo linear arithmetic SUP(LA)
• Refutational theorem proving for hierarchic first-order theories
• Finite Quantification in Hierarchic Theorem Proving

Cited in

(19)

• Superposition decides the first-order logic fragment over ground theories
• An efficient subsumption test pipeline for BS(LRA) clauses
• Superposition of snarks revisited
• Deciding the Bernays-Schoenfinkel fragment over bounded difference constraints by simple clause learning over theories
• Integrating Linear Arithmetic into Superposition Calculus
• Superposition modulo linear arithmetic SUP(LA)
• scientific article; zbMATH DE number 1300967 (Why is no real title available?)
• scientific article; zbMATH DE number 810189 (Why is no real title available?)
• scientific article; zbMATH DE number 881986 (Why is no real title available?)
• Hierarchic superposition with weak abstraction
• Formalizing Bachmair and Ganzinger's ordered resolution prover
• A comprehensive framework for saturation theorem proving
• Symbolic Model Construction for Saturated Constrained Horn Clauses
• ALASCA: reasoning in quantified linear arithmetic
• A modular formalization of superposition in Isabelle/HOL
• Computing witnesses using the SCAN algorithm
• Elimination of composite superpositions may cause abortion
• A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic
• Symbol elimination and applications to parametric entailment problems

This page was built for publication: Hierarchic superposition revisited

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2185457)