Labelled splitting
From MaRDI portal
Publication:1037396
DOI10.1007/S10472-009-9150-9zbMATH Open1192.68628OpenAlexW2914680778MaRDI QIDQ1037396FDOQ1037396
Authors: 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
Recommendations
Cites Work
- Theory and Applications of Satisfiability Testing
- The TPTP problem library. CNF release v1. 2. 1
- Decision Procedures for SAT, SAT Modulo Theories and Beyond. The BarcelogicTools
- Resolution theorem proving
- Term Rewriting and All That
- A Computing Procedure for Quantification Theory
- The model evolution calculus as a first-order DPLL method
- Resolution decision procedures
- Combining superposition, sorts and splitting
- Labelled Splitting
- Computing small clause normal forms
- Paramodulation-based theorem proving
- Splitting through new proposition symbols
- System Description: Spass Version 3.0
- Title not available (Why is that?)
- Labelled Clauses
Cited In (16)
- Labelled Clauses
- Superposition for bounded domains
- Almost free splitters
- A comprehensive framework for saturation theorem proving
- Unifying splitting
- Playing with AVATAR
- A comprehensive framework for saturation theorem proving
- Case splitting in an automatic theorem prover for real-valued special functions
- A PLTL-prover based on labelled superposition with partial model guidance
- Combining superposition, sorts and splitting
- SAT-Inspired Eliminations for Superposition
- A unifying splitting framework
- A Labelled System for IPL with Variable Splitting
- NRCL -- a model building approach to the Bernays-Schönfinkel fragment
- Labelled Splitting
- Labelled unit superposition calculi for instantiation-based reasoning
Uses Software
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)
