The disconnection tableau calculus

DOI10.1007/S10817-006-9048-8zbMATH Open1121.03022OpenAlexW2079576159MaRDI QIDQ877889FDOQ877889

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

Recommendations

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

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• lean\(T^ AP\): Lean tableau-based deduction
• Title not available (Why is that?)
• Title not available (Why is that?)
• Term Rewriting and All That
• A Machine-Oriented Logic Based on the Resolution Principle
• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving
• Ordered semantic hyper-linking
• Rewriting
• Proof and Model Generation with Disconnection Tableaux
• An improved proof procedure1
• Title not available (Why is that?)
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Eliminating dublication with the hyper-linking strategy
• Paramodulation-based theorem proving
• Title not available (Why is that?)
• Title not available (Why is that?)
• Automated Deduction – CADE-20
• Automated Deduction – CADE-19
• Title not available (Why is that?)
• Theorem Proving via General Matings
• Depth-first proof search without backtracking for free-variable clausal tableaux
• Basic narrowing revisited
• On Matrices with Connections
• Proving Theorems with the Modification Method
• Title not available (Why is that?)
• Refutation graphs
• Controlled integration of the cut rule into connection tableau calculi
• Partial instantiation methods for inference in first-order logic
• Title not available (Why is that?)
• A nucleus of a theorem-prover described inAlgol-68
• Title not available (Why is that?)
• Title not available (Why is that?)
• Automated Reasoning with Analytic Tableaux and Related Methods
• Automated Reasoning
• Title not available (Why is that?)

Cited In (6)

• Connection tableau calculi with disjunctive constraints
• Connection Tableaux with Lazy Paramodulation
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Connection tableau calculi with disjunctive contraints (TU München)

Uses Software

• SETHEO
• SATO
• GrAnDe
• SATCHMO
• DCTP
• E-SETHEO
• leanTAP
• 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)