Hierarchic superposition revisited

DOI10.1007/978-3-030-22102-7_2zbMath1443.68212arXiv1904.03776OpenAlexW2577664989MaRDI QIDQ2185457

Uwe Waldmann, Peter Baumgartner

Publication date: 4 June 2020

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

zbMATH Keywords

automated deductionsuperposition calculuscombinations of theories

Mathematics Subject Classification ID

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

Related Items (6)

A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic ⋮ Symbol elimination and applications to parametric entailment problems ⋮ Deciding the Bernays-Schoenfinkel fragment over bounded difference constraints by simple clause learning over theories ⋮ Formalizing Bachmair and Ganzinger's ordered resolution prover ⋮ A comprehensive framework for saturation theorem proving ⋮ An efficient subsumption test pipeline for BS(LRA) clauses

This page was built for publication: Hierarchic superposition revisited