A Model Generation Style Completeness Proof for Constraint Tableaux with Superposition

摘要

We present a calculus that integrates equality handling by superposition into a free variable tableau calculus. We prove completeness of this calculus by an adaptation of the model generation [2,15] technique commonly used for completeness proofs of resolution calculi. The calculi and the completeness proof are compared to earlier results of Degtyarev and Voronkov [7].