On Unit-Refutation Complete Formulae with Existentially Quantified Variables

We analyze, along the lines of the knowledge compilation map, both the tractability and the succinctness of the propositional language URC-C of unit-refutation complete propositional formulae, as well as its disjunctive closure URC-C[OR; EXISTS], and a superset of URC-C

where variables can be existentially quantified and unit-refutation completeness concerns only consequences built up from free variables.

urc.pdf
PDF file

In  Principles of Knowledge Representation and Reasoning (KR 2012)

Publisher  Association for the Advancement of Artificial Intelligence

Details

TypeInproceedings
> Publications > On Unit-Refutation Complete Formulae with Existentially Quantified Variables