• search hit 129 of 143
Back to Result List

Tableaux between proving, projection and compilation

  • 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.

Download full text files

Export metadata

Additional Services

Share in Twitter Search Google Scholar
Author:Christoph Wernhard
Series (Volume no.):Arbeitsberichte, FB Informatik (2007,18)
Document Type:Part of Periodical
Date of completion:2007/07/06
Date of publication:2007/07/06
Publishing institution:Universität Koblenz-Landau, Campus Koblenz, Universitätsbibliothek
Release Date:2007/07/06
Tag:Automated Theorem Proving; Knowledge Compilation
Number of pages:31
Institutes:Fachbereich 4 / Fachbereich 4
Fachbereich 4 / Institut für Informatik
Dewey Decimal Classification:0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 004 Datenverarbeitung; Informatik
Licence (German):License LogoEs gilt das deutsche Urheberrecht: § 53 UrhG