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

• Type: Journal
• Year: 2007
• Where: JAR
• Authors: Martin Giese
• Keywords: Completeness Proof, JAR 2007, Ordered Superposition Rules, Superposition Rules