A unifying splitting framework
From MaRDI portal
Publication:2055869
DOI10.1007/978-3-030-79876-5_20OpenAlexW3177951153MaRDI QIDQ2055869FDOQ2055869
Authors: Gabriel Ebner, Jasmin Christian Blanchette, Sophie Tourret
Publication date: 1 December 2021
Full work available at URL: https://doi.org/10.1007/978-3-030-79876-5_20
Recommendations
Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Cites Work
- Resolution theorem proving
- Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
- Title not available (Why is that?)
- Satisfiability modulo theories and assignments
- Combining superposition, sorts and splitting
- Concrete semantics. With Isabelle/HOL
- A model-constructing satisfiability calculus
- 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
- AVATAR: The Architecture for First-Order Theorem Provers
- Labelled splitting
- A unifying splitting framework
- The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
- Revisiting enumerative instantiation
- Playing with AVATAR
- A comprehensive framework for saturation theorem proving
Cited In (10)
- Splitting Enables Overcoming the Curse of Dimensionality
- The Finest Splitting Uniformity
- Making higher-order superposition work
- Title not available (Why is that?)
- Unifying splitting
- The split-BREAK model
- Making higher-order superposition work
- A comprehensive framework for saturation theorem proving
- A unifying splitting framework
- A Labelled System for IPL with Variable Splitting
Uses Software
This page was built for publication: A unifying splitting framework
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2055869)