Sciweavers

Share
JAR
2007

Superposition-based Equality Handling for Analytic Tableaux

11 years 1 months ago
Superposition-based Equality Handling for Analytic Tableaux
We present a variant of the basic ordered superposition rules to handle equality in an analytic free-variable tableau calculus. We prove completeness of this calculus by an adaptation of the model generation technique commonly used for completeness proofs of superposition in the context of resolution calculi. The calculi and the completeness proof are compared to earlier results of Degtyarev and Voronkov. Some variations and refinements are discussed. Key words superposition rules · equality handling · analytic tableaux
Martin Giese
Added 15 Dec 2010
Updated 15 Dec 2010
Type Journal
Year 2007
Where JAR
Authors Martin Giese
Comments (0)
books