The disconnection method
From MaRDI portal
Publication:4645231
DOI10.1007/3-540-61208-4_8zbMath1412.68210OpenAlexW960765268MaRDI QIDQ4645231
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
Related Items
Semantically-guided goal-sensitive reasoning: model representation, History and Prospects for First-Order Automated Deduction, The model evolution calculus as a first-order DPLL method, Depth-first proof search without backtracking for free-variable clausal tableaux, Model evolution with equality -- revised and implemented, Semantically-guided goal-sensitive reasoning: inference system and completeness, Towards a unified model of search in theorem-proving: subgoal-reduction strategies, Lemma matching for a PTTP-based top-down theorem prover, Hyper tableaux, Set of support, demodulation, paramodulation: a historical perspective
Uses Software
Cites Work
- How to avoid the derivation of redundant clauses in reasoning systems
- Seventy-five problems for testing automatic theorem provers
- Errata to ``75 problems for testing automatic theorem provers
- Controlled integration of the cut rule into connection tableau calculi
- lean\(T^ AP\): Lean tableau-based deduction
- Proving Theorems with the Modification Method
- Unnamed Item
- Unnamed Item
- Unnamed Item
