A unifying splitting framework
From MaRDI portal
Publication:2055869
Recommendations
Cites work
- scientific article; zbMATH DE number 3299786 (Why is no real title available?)
- A comprehensive framework for saturation theorem proving
- A model-constructing satisfiability calculus
- A unifying splitting framework
- AVATAR: The Architecture for First-Order Theorem Provers
- Combining superposition, sorts and splitting
- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
- Concrete semantics. With Isabelle/HOL
- Labelled splitting
- On Deciding Satisfiability by DPLL( $\Gamma+{\mathcal T}$ ) and Unsound Theorem Proving
- Playing with AVATAR
- Quantifier instantiation techniques for finite model finding in SMT
- Resolution theorem proving
- Revisiting enumerative instantiation
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- Satisfiability modulo theories and assignments
- Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
- The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
Cited in
(10)- Splitting Enables Overcoming the Curse of Dimensionality
- The Finest Splitting Uniformity
- Making higher-order superposition work
- scientific article; zbMATH DE number 2125665 (Why is no real title available?)
- The split-BREAK model
- Unifying splitting
- Making higher-order superposition work
- A comprehensive framework for saturation theorem proving
- A unifying splitting framework
- A Labelled System for IPL with Variable Splitting
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)