Labelled splitting

DOI10.1007/S10472-009-9150-9MaRDI QIDQ1037396zbMATH OpenOpenAlexFDO

Authors Arnaud Fietzke, Christoph Weidenbach

Publication date 16 November 2009

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

Copyright license Creative Commons Attribution-NonCommercial 4.0 International

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

zbMATH Keywords

clause learningsuperposition calculus

Mathematics Subject Classification ID

Recommendations

• Labelled Splitting
• Combining superposition, sorts and splitting
• Splitting through new proposition symbols
• A combined superposition and model evolution calculus
• Superposition and Model Evolution Combined

Cites work

• scientific article; zbMATH DE number 517065 (Why is no real title available?)
• A Computing Procedure for Quantification Theory
• Combining superposition, sorts and splitting
• Computing small clause normal forms
• Decision Procedures for SAT, SAT Modulo Theories and Beyond. The BarcelogicTools
• Labelled Clauses
• Labelled Splitting
• Paramodulation-based theorem proving
• Resolution decision procedures
• Resolution theorem proving
• Splitting through new proposition symbols
• System Description: Spass Version 3.0
• Term Rewriting and All That
• The TPTP problem library. CNF release v1. 2. 1
• The model evolution calculus as a first-order DPLL method
• Theory and Applications of Satisfiability Testing

Cited in

(16)

• Unifying splitting
• Labelled unit superposition calculi for instantiation-based reasoning
• A PLTL-prover based on labelled superposition with partial model guidance
• A comprehensive framework for saturation theorem proving
• A Labelled System for IPL with Variable Splitting
• Case splitting in an automatic theorem prover for real-valued special functions
• Superposition for bounded domains
• Playing with AVATAR
• Combining superposition, sorts and splitting
• Almost free splitters
• SAT-Inspired Eliminations for Superposition
• A comprehensive framework for saturation theorem proving
• A unifying splitting framework
• NRCL -- a model building approach to the Bernays-Schönfinkel fragment
• Labelled Splitting
• Labelled Clauses

Describes a project that uses

Uses Software

• SPASS
• TPTP
• FLOTTER

This page was built for publication: Labelled splitting

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1037396)