The disconnection method
From MaRDI portal
Publication:4645231
DOI10.1007/3-540-61208-4_8zbMATH Open1412.68210OpenAlexW960765268MaRDI QIDQ4645231FDOQ4645231
Authors: Jean-Paul Billon 
Publication date: 10 January 2019
Published in: Theorem Proving with Analytic Tableaux and Related Methods (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/3-540-61208-4_8
Recommendations
Cites Work
- lean\(T^ AP\): Lean tableau-based deduction
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- How to avoid the derivation of redundant clauses in reasoning systems
- Proving Theorems with the Modification Method
- Seventy-five problems for testing automatic theorem provers
- Controlled integration of the cut rule into connection tableau calculi
- Errata to ``75 problems for testing automatic theorem provers
Cited In (13)
- Set of support, demodulation, paramodulation: a historical perspective
- Connection tableau calculi with disjunctive constraints
- Lemma matching for a PTTP-based top-down theorem prover
- Semantically-guided goal-sensitive reasoning: inference system and completeness
- Semantically-guided goal-sensitive reasoning: model representation
- The disconnection tableau calculus
- Depth-first proof search without backtracking for free-variable clausal tableaux
- Model evolution with equality -- revised and implemented
- The model evolution calculus as a first-order DPLL method
- Towards a unified model of search in theorem-proving: subgoal-reduction strategies
- History and prospects for first-order automated deduction
- Automated Reasoning
- Hyper tableaux
Uses Software
This page was built for publication: The disconnection method
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4645231)
