Existential Closures for Knowledge Compilation
Pierre Marquis
We study the existential closures of several propositional languages $\mathcal{L}$ considered recently as target languages for knowledge compilation (KC). We analyze the queries, transformations, expressiveness and succinctness of the resulting languages $\mathcal{L}[\exists]$ in order to locate them in the KC map. As a by-product, we also address several issues concerning disjunction closures that were left open so far. From our investigation, the language $\horn[\vee,\exists]$ (where disjunctions and existential quantifications can be applied to Horn CNF formulae) appears as an interesting target language for the KC purpose, challenging the influential DNNF languages, as well as the disjunction closure \aff[$\vee$] of affine formulae.