The disconnection tableau calculus
From MaRDI portal
Publication:877889
DOI10.1007/s10817-006-9048-8zbMath1121.03022MaRDI QIDQ877889
Publication date: 4 May 2007
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-006-9048-8
03B35: Mechanization of proofs and logical operations
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Eliminating dublication with the hyper-linking strategy
- Refutation graphs
- Controlled integration of the cut rule into connection tableau calculi
- Depth-first proof search without backtracking for free-variable clausal tableaux
- Ordered semantic hyper-linking
- Partial instantiation methods for inference in first-order logic
- Basic narrowing revisited
- lean\(T^ AP\): Lean tableau-based deduction
- Proof and Model Generation with Disconnection Tableaux
- An improved proof procedure1
- Theorem Proving via General Matings
- On Matrices with Connections
- Proving Theorems with the Modification Method
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- A nucleus of a theorem-prover described inAlgol-68
- Term Rewriting and All That
- Automated Reasoning with Analytic Tableaux and Related Methods
- Automated Reasoning
- Automated Deduction – CADE-20
- A Machine-Oriented Logic Based on the Resolution Principle
- A Computing Procedure for Quantification Theory
- A machine program for theorem-proving
- Automated Deduction – CADE-19
