A unifying splitting framework

DOI10.1007/978-3-030-79876-5_20MaRDI QIDQ2055869zbMATH OpenOpenAlexFDO

Authors Gabriel Ebner, Jasmin Christian Blanchette, Sophie Tourret

Publication date 1 December 2021

Copyright license Creative Commons Attribution 4.0 International

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)

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

Cites work

• 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
• scientific article; zbMATH DE number 3299786 (Why is no real title available?)
• 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)

• A unifying splitting framework
• scientific article; zbMATH DE number 2125665 (Why is no real title available?)
• A Labelled System for IPL with Variable Splitting
• The Finest Splitting Uniformity
• The split-BREAK model
• Splitting Enables Overcoming the Curse of Dimensionality
• Making higher-order superposition work
• Making higher-order superposition work
• A comprehensive framework for saturation theorem proving
• Unifying splitting

Describes a project that uses

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)