A comprehensive framework for saturation theorem proving

DOI10.1007/978-3-030-51074-9_18OpenAlexW3039562913MaRDI QIDQ5918558

Jasmin Christian Blanchette, Sophie Tourret, Uwe Waldmann, Simon Robillard

Publication date: 9 November 2022

Published in: Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-030-51074-9_18

Mathematics Subject Classification ID

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

Related Items

Implementing Superposition in iProver (System Description), Unnamed Item, Unifying splitting, Saturation-based Boolean conjunctive query answering and rewriting for the guarded quantification fragments, Superposition for higher-order logic, SCL(EQ): SCL for first-order logic with equality, Formalizing Bachmair and Ganzinger's ordered resolution prover, Superposition with lambdas, Making higher-order superposition work, A comprehensive framework for saturation theorem proving, A unifying splitting framework, Superposition with first-class booleans and inprocessing clausification, Superposition for full higher-order logic, A comprehensive framework for saturation theorem proving, Set of support, demodulation, paramodulation: a historical perspective, Ground joinability and connectedness in the superposition calculus, SCL(EQ): SCL for first-order logic with equality, SAT-Inspired Eliminations for Superposition

Uses Software

• Isabelle/HOL
• OTTER
• VAMPIRE
• E Theorem Prover
• Locales
• Waldmeister
• DISCOUNT
• Archive Formal Proofs
• AVATAR
• Ordered_Resolution_Prover

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Labelled splitting
• Refutational theorem proving for hierarchic first-order theories
• Isabelle/HOL. A proof assistant for higher-order logic
• Superposition for \(\lambda\)-free higher-order logic
• Superposition with datatypes and codatatypes
• Cancellative Abelian monoids and related structures in refutational theorem proving. I
• Theorem proving with ordering and equality constrained clauses
• A combinator-based superposition calculus for higher-order logic
• Locales: a module system for mathematical theories
• Truly Modular (Co)datatypes for Isabelle/HOL
• AVATAR: The Architecture for First-Order Theorem Provers
• Concrete Semantics
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• Formalizing Bachmair and Ganzinger's ordered resolution prover
• A comprehensive framework for saturation theorem proving
• Superposition with lambdas