On Unit-Refutation Complete Formulae with Existentially Quantified Variables
Bordeaux, Lucas (Microsoft Research, Cambridge) | Janota, Mikolas (INESC-ID, Lisboa) | Marques-Silva, Joao (University College Dublin) | Marquis, Pierre (CRIL-CNRS, University of Artois)
We analyze, along the lines of the knowledge compilation map, both the tractability and the succinctness of the propositional language URC of unit-refutation complete propositional formulae, as well as its disjunctive closure URC[V, ∃], and a superset of URC where variables can be existentially quantified and unit-refutation completeness concerns only consequences built up from free variables.
- Technology: