A unifying splitting framework

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

• Playing with AVATAR
• AVATAR: The Architecture for First-Order Theorem Provers
• Cooperating proof attempts
• Combining superposition, sorts and splitting
• The 481 ways to split a clause and deal with propositional variables

Mathematics Subject Classification ID

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

• Isabelle/HOL
• OTTER
• TPTP
• AVATAR

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)