Labelled splitting

DOI10.1007/s10472-009-9150-9zbMath1192.68628OpenAlexW2914680778MaRDI QIDQ1037396

Arnaud Fietzke, Christoph Weidenbach

Publication date: 16 November 2009

Published in: Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10472-009-9150-9

zbMATH Keywords

clause learningsuperposition calculus

Mathematics Subject Classification ID

Related Items (8)

Case splitting in an automatic theorem prover for real-valued special functions ⋮ Unifying splitting ⋮ NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment ⋮ Superposition for Bounded Domains ⋮ A comprehensive framework for saturation theorem proving ⋮ A unifying splitting framework ⋮ A comprehensive framework for saturation theorem proving ⋮ SAT-Inspired Eliminations for Superposition

Uses Software

• SPASS
• TPTP
• FLOTTER

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The TPTP problem library. CNF release v1. 2. 1
• The model evolution calculus as a first-order DPLL method
• Splitting through New Proposition Symbols
• Labelled Splitting
• Labelled Clauses
• System Description: Spass Version 3.0
• Term Rewriting and All That
• Theory and Applications of Satisfiability Testing
• Decision Procedures for SAT, SAT Modulo Theories and Beyond. The BarcelogicTools
• A Computing Procedure for Quantification Theory

This page was built for publication: Labelled splitting