Existential Closures for Knowledge Compilation

We study the existential closures of several propositional languages L considered recently as target languages for knowledge compilation (KC), namely the incomplete fragments KROM-C, HORN-C, K/H-C, renH-C, AFF, and the corresponding disjunction closures KROM-C[V], HORN-C[V], K/H-C[V], renH-C[V], and AFF[V]. We analyze the queries, transformations, expressiveness and succinctness of the resulting languages L[E] 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-C[V, E] (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.