caa a22 4500 463182774 CHVBK 20180406164844.0 cr unu---uuuuu 170326e20070401xx s 000 0 eng 10.1007/s10817-006-9048-8 doi (NATIONALLICENCE)springer-10.1007/s10817-006-9048-8 The Disconnection Tableau Calculus [Elektronische Daten] [Reinhold Letz, Gernot Stenz] In this paper we give a comprehensive presentation of the disconnection tableau calculus, a proof method for formulas in classical first-order clause logic. The distinguishing property of this calculus is that it uses unification in such a manner that important proof-theoretic advantages of the classical (i.e., Smullyan-style) tableau calculus are preserved, specifically the termination and model generation characteristics for certain formula classes. Additionally, the calculus is well suited for fully automated proof search. The calculus is described in detail with soundness and completeness proofs, and a number of important calculus refinements developed over the past years are presented. Referring to the model-finding abilities of the disconnection calculus, we explain the extraction and representation of models. We also describe the integration of paramodulation-based equality handling. Finally, we give an overview of related methods. Springer Science+Business Media, Inc., 2006 disconnection tableaux nationallicence theorem proving nationallicence Letz Reinhold Institut für Informatik, Technische Universität München, D-85748, Garching, Germany aut Stenz Gernot Institut für Informatik, Technische Universität München, D-85748, Garching, Germany aut Journal of Automated Reasoning Kluwer Academic Publishers 38/1-3(2007-04-01), 79-126 0168-7433 38:1-3<79 2007 38 10817 https://doi.org/10.1007/s10817-006-9048-8 text/html Onlinezugriff via DOI 1 research-article jats NATIONALLICENCE 856 40 https://doi.org/10.1007/s10817-006-9048-8 text/html Onlinezugriff via DOI NATIONALLICENCE 700 1- Letz Reinhold Institut für Informatik, Technische Universität München, D-85748, Garching, Germany aut NATIONALLICENCE 700 1- Stenz Gernot Institut für Informatik, Technische Universität München, D-85748, Garching, Germany aut NATIONALLICENCE 773 0- Journal of Automated Reasoning Kluwer Academic Publishers 38/1-3(2007-04-01), 79-126 0168-7433 38:1-3<79 2007 38 10817 Metadata rights reserved Springer special CC-BY-NC licence nationallicence BK010053 XK010053 XK010000 NATIONALLICENCE NATIONALLICENCE NL-springer