Tableaux for Projection Computation and Knowledge Compilation

11 years 6 months ago
Tableaux for Projection Computation and Knowledge Compilation
Projection computation is a generalization of second-order quantifier elimination, which in turn is closely related to the computation of forgetting and of uniform interpolants. On the basis of a unified view on projection computation and knowledge compilation, we develop a framework for applying tableau methods to these tasks. It takes refinements from performance oriented systems into account. Formula simplifications are incorporated at the level of tableau structure modification, and at the level of simplifying encountered subformulas that are not yet fully compiled. In particular, such simplifications can involve projection computation, where this is possible with low cost. We represent tableau construction by means of rewrite rules on formulas, extended with some auxiliary functors, which is particularly convenient for formula transformation tasks. As instantiations of the framework, we discuss approaches to propositional knowledge compilation from the literature, including ...
Christoph Wernhard
Added 27 Jul 2010
Updated 27 Jul 2010
Type Conference
Year 2009
Authors Christoph Wernhard
Comments (0)