caa a22 4500 463182707 CHVBK 20180406164843.0 cr unu---uuuuu 170326e20070401xx s 000 0 eng 10.1007/s10817-006-9050-1 doi (NATIONALLICENCE)springer-10.1007/s10817-006-9050-1 Giese Martin Johann Radon Institute for Computational and Applied Mathematics, Austrian Academy of Sciences, Altenbergerstr. 69, A-4040, Linz, Austria aut Superposition-based Equality Handling for Analytic Tableaux [Elektronische Daten] [Martin Giese] 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. Springer Science+Business Media, Inc., 2006 superposition rules nationallicence equality handling nationallicence analytic tableaux nationallicence Journal of Automated Reasoning Kluwer Academic Publishers 38/1-3(2007-04-01), 127-153 0168-7433 38:1-3<127 2007 38 10817 https://doi.org/10.1007/s10817-006-9050-1 text/html Onlinezugriff via DOI 1 research-article jats NATIONALLICENCE 856 40 https://doi.org/10.1007/s10817-006-9050-1 text/html Onlinezugriff via DOI NATIONALLICENCE 100 1- Giese Martin Johann Radon Institute for Computational and Applied Mathematics, Austrian Academy of Sciences, Altenbergerstr. 69, A-4040, Linz, Austria aut NATIONALLICENCE 773 0- Journal of Automated Reasoning Kluwer Academic Publishers 38/1-3(2007-04-01), 127-153 0168-7433 38:1-3<127 2007 38 10817 Metadata rights reserved Springer special CC-BY-NC licence nationallicence BK010053 XK010053 XK010000 NATIONALLICENCE NATIONALLICENCE NL-springer