The disconnection tableau calculus

DOI10.1007/S10817-006-9048-8MaRDI QIDQ877889zbMATH OpenOpenAlexFDO

Authors 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)

Recommendations

• Proof and model generation with disconnection tableaux
• Automated Reasoning
• The disconnection method
• scientific article; zbMATH DE number 1950261
• Universal variables in disconnection tableaux

Cites work

• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving
• A Machine-Oriented Logic Based on the Resolution Principle
• A nucleus of a theorem-prover described inAlgol-68
• An improved proof procedure1
• Automated Deduction – CADE-20
• Automated Reasoning
• Basic narrowing revisited
• Controlled integration of the cut rule into connection tableau calculi
• Depth-first proof search without backtracking for free-variable clausal tableaux
• Eliminating dublication with the hyper-linking strategy
• scientific article; zbMATH DE number 3904558 (Why is no real title available?)
• scientific article; zbMATH DE number 4094866 (Why is no real title available?)
• scientific article; zbMATH DE number 1189096 (Why is no real title available?)
• scientific article; zbMATH DE number 1189106 (Why is no real title available?)
• scientific article; zbMATH DE number 1341619 (Why is no real title available?)
• scientific article; zbMATH DE number 1950261 (Why is no real title available?)
• scientific article; zbMATH DE number 1950272 (Why is no real title available?)
• scientific article; zbMATH DE number 1552522 (Why is no real title available?)
• scientific article; zbMATH DE number 1552523 (Why is no real title available?)
• scientific article; zbMATH DE number 1552529 (Why is no real title available?)
• scientific article; zbMATH DE number 1552532 (Why is no real title available?)
• scientific article; zbMATH DE number 1765683 (Why is no real title available?)
• scientific article; zbMATH DE number 194631 (Why is no real title available?)
• scientific article; zbMATH DE number 2090306 (Why is no real title available?)
• scientific article; zbMATH DE number 837700 (Why is no real title available?)
• scientific article; zbMATH DE number 3274715 (Why is no real title available?)
• scientific article; zbMATH DE number 3407195 (Why is no real title available?)
• lean\(T^ AP\): Lean tableau-based deduction
• On Matrices with Connections
• Ordered semantic hyper-linking
• Paramodulation-based theorem proving
• Partial instantiation methods for inference in first-order logic
• Proof and model generation with disconnection tableaux
• Proving Theorems with the Modification Method
• Refutation graphs
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• Rewriting
• Simplification rules for constrained formula tableaux
• Term Rewriting and All That
• The model evolution calculus.
• Theorem Proving via General Matings

Cited in

(13)

• Connection tableau calculi with disjunctive constraints
• Certification of nonclausal connection tableaux proofs
• scientific article; zbMATH DE number 1612557 (Why is no real title available?)
• Connection tableau calculi with disjunctive contraints (TU München)
• Proof and model generation with disconnection tableaux
• Connection Tableaux with Lazy Paramodulation
• scientific article; zbMATH DE number 1950272 (Why is no real title available?)
• scientific article; zbMATH DE number 1765683 (Why is no real title available?)
• The disconnection method
• Universal variables in disconnection tableaux
• Automated Reasoning
• Automated Reasoning with Analytic Tableaux and Related Methods
• Connection tableaux with lazy paramodulation

Describes a project that uses

Uses Software

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

This page was built for publication: The disconnection tableau calculus

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q877889)