author = {Martin Giese},
title = {{Superposition-based Equality Handling for Analytic Tableaux}},
language = {english},
abstract = {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. },
journal = {Journal of Automated Reasoning},
volume = {38},
number = {1-3},
pages = {127--153},
isbn_issn = {1573-0670},
year = {2006},
month = {December},
note = {Appeared online 2 December 2006, in print April 2007},
refereed = {yes},
length = {27},
url = {http://dx.doi.org/10.1007/s10817-006-9050-1}