TY - GEN A1 - Wernhard, Christoph T1 - Tableaux between proving, projection and compilation N2 - Generalized methods for automated theorem proving can be used to compute formula transformations such as projection elimination and knowledge compilation. We present a framework based on clausal tableaux suited for such tasks. These tableaux are characterized independently of particular construction methods, but important features of empirically successful methods are taken into account, especially dependency directed backjumping and branch local operation. As an instance of that framework an adaption of DPLL is described. We show that knowledge compilation methods can be essentially improved by weaving projection elimination partially into the compilation phase. T3 - Arbeitsberichte, FB Informatik - 2007,18 KW - Knowledge Compilation KW - Automated Theorem Proving Y1 - 2007 UR - https://kola.opus.hbz-nrw.de/frontdoor/index/index/docId/125 UR - https://nbn-resolving.org/urn:nbn:de:kola-1258 ER -