There are several different methods which try to decide unsatisfiability of a set of clauses by generating an unsatisfiable set of instances of the input clauses. We consider the \emph{Disconnection Tableau Calculus}, \emph{Primal Partial Instantiation} and \emph{Resolution-Based Instance-Generation}, all of which can be seen as refinements of the clause linking approach. We present these three methods accurately and in a consistent manner. Similarities and equivalences of the methods will be pointed out and we will show if proofs of one calculus can be simulated by a different method, generating only instances from the given proof.
Editor(s) Swen Jacobs | Created 03/10/2005 02:46:19 PM | |
Revision 1. 0. | Editor Christine Kiesel Swen Jacobs | Edit Date 27.04.2005 10:31:09 03/10/2005 02:46:19 PM |