Unifying splitting
From MaRDI portal
Publication:6103590
DOI10.1007/s10817-023-09660-8OpenAlexW4367300294MaRDI QIDQ6103590
Gabriel Ebner, Jasmin Christian Blanchette, Sophie Tourret
Publication date: 27 June 2023
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-023-09660-8
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Labelled splitting
- A unifying splitting framework
- Subsumption demodulation in first-order theorem proving
- 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
- SPASS & FLOTTER version 0.42
- On Deciding Satisfiability by DPLL( $\Gamma+{\mathcal T}$ ) and Unsound Theorem Proving
- A Machine-Oriented Logic Based on the Resolution Principle
- A comprehensive framework for saturation theorem proving
This page was built for publication: Unifying splitting
