Comparing Instance Generation Methods for Automated Reasoning

摘要

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 proposi-tionally 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.