A unifying splitting framework

DOI10.1007/978-3-030-79876-5_20OpenAlexW3177951153MaRDI QIDQ2055869

Jasmin Christian Blanchette, Gabriel Ebner, Sophie Tourret

Publication date: 1 December 2021

Full work available at URL: https://doi.org/10.1007/978-3-030-79876-5_20

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items

Unifying splitting ⋮ Making higher-order superposition work ⋮ Making higher-order superposition work ⋮ A unifying splitting framework ⋮ A comprehensive framework for saturation theorem proving

Uses Software

• Isabelle/HOL
• OTTER
• TPTP
• AVATAR

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Labelled splitting
• The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
• A unifying splitting framework
• Revisiting enumerative instantiation
• Satisfiability modulo theories and assignments
• AVATAR: The Architecture for First-Order Theorem Provers
• Concrete Semantics
• A Model-Constructing Satisfiability Calculus
• Playing with AVATAR
• Solving SAT and SAT Modulo Theories
• Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• Quantifier Instantiation Techniques for Finite Model Finding in SMT
• On Deciding Satisfiability by DPLL( $\Gamma+{\mathcal T}$ ) and Unsound Theorem Proving
• A comprehensive framework for saturation theorem proving