The disconnection tableau calculus

DOI10.1007/s10817-006-9048-8zbMath1121.03022OpenAlexW2079576159MaRDI QIDQ877889

Reinhold Letz, Gernot Stenz

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

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Uses Software

• SETHEO
• SATO
• GrAnDe
• SATCHMO
• DCTP
• E-SETHEO
• leanTAP
• 3TAP
• HARP

Cites Work

• 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
• 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