AAAI Publications, Thirteenth International Conference on the Principles of Knowledge Representation and Reasoning

Font Size: 
On Unit-Refutation Complete Formulae with Existentially Quantified Variables
Lucas Bordeaux, Mikolas Janota, Joao Marques-Silva, Pierre Marquis

Last modified: 2012-05-17


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.


Knowledge Compilation, Propositional Logic, Conjunctive Normal Form

Full Text: PDF