Recommendations
Cites work
- Controlled integration of the cut rule into connection tableau calculi
- Errata to ``75 problems for testing automatic theorem provers
- How to avoid the derivation of redundant clauses in reasoning systems
- scientific article; zbMATH DE number 46359 (Why is no real title available?)
- scientific article; zbMATH DE number 194631 (Why is no real title available?)
- scientific article; zbMATH DE number 3415409 (Why is no real title available?)
- lean\(T^ AP\): Lean tableau-based deduction
- Proving Theorems with the Modification Method
- Seventy-five problems for testing automatic theorem provers
Cited in
(13)- Depth-first proof search without backtracking for free-variable clausal tableaux
- Connection tableau calculi with disjunctive constraints
- Semantically-guided goal-sensitive reasoning: inference system and completeness
- Set of support, demodulation, paramodulation: a historical perspective
- The model evolution calculus as a first-order DPLL method
- Towards a unified model of search in theorem-proving: subgoal-reduction strategies
- Semantically-guided goal-sensitive reasoning: model representation
- History and prospects for first-order automated deduction
- Model evolution with equality -- revised and implemented
- Lemma matching for a PTTP-based top-down theorem prover
- Hyper tableaux
- Automated Reasoning
- The disconnection tableau calculus
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)
