caa a22 4500 463182715 CHVBK 20180406164843.0 cr unu---uuuuu 170326e20070401xx s 000 0 eng 10.1007/s10817-006-9046-x doi (NATIONALLICENCE)springer-10.1007/s10817-006-9046-x Comparing Instance Generation Methods for Automated Reasoning [Elektronische Daten] [Swen Jacobs, Uwe Waldmann] The clause-linking technique of Lee and Plaisted proves the unsatisfiability of a set of first-order clauses by generating a sufficiently large set of instances of these clauses that can be shown to be propositionally unsatisfiable. In recent years, this approach has been refined in several directions, leading to both tableau-based methods, such as the disconnection tableau calculus, and saturation-based methods, such as primal partial instantiation and resolution-based instance generation. We investigate the relationship between these calculi and answer the question to what extent refutation or consistency proofs in one calculus can be simulated in another one. Springer Science+Business Media, Inc., 2006 automated reasoning nationallicence theorem proving nationallicence disconnection calculus nationallicence primal partial instantiation nationallicence resolution-based instance generation nationallicence Jacobs Swen Max-Planck-Institut für Informatik, Saarbrücken, Germany aut Waldmann Uwe Max-Planck-Institut für Informatik, Saarbrücken, Germany aut Journal of Automated Reasoning Kluwer Academic Publishers 38/1-3(2007-04-01), 57-78 0168-7433 38:1-3<57 2007 38 10817 https://doi.org/10.1007/s10817-006-9046-x text/html Onlinezugriff via DOI 1 research-article jats NATIONALLICENCE 856 40 https://doi.org/10.1007/s10817-006-9046-x text/html Onlinezugriff via DOI NATIONALLICENCE 700 1- Jacobs Swen Max-Planck-Institut für Informatik, Saarbrücken, Germany aut NATIONALLICENCE 700 1- Waldmann Uwe Max-Planck-Institut für Informatik, Saarbrücken, Germany aut NATIONALLICENCE 773 0- Journal of Automated Reasoning Kluwer Academic Publishers 38/1-3(2007-04-01), 57-78 0168-7433 38:1-3<57 2007 38 10817 Metadata rights reserved Springer special CC-BY-NC licence nationallicence BK010053 XK010053 XK010000 NATIONALLICENCE NATIONALLICENCE NL-springer