On Unit-Refutation Complete Formulae with Existentially Quantified Variables

Lucas Bordeaux, Mikolas Janota, Joao Marques-Silva, and Pierre Marquis

Abstract

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.

Details

Publication typeInproceedings
Published inPrinciples of Knowledge Representation and Reasoning (KR 2012)
PublisherAssociation for the Advancement of Artificial Intelligence
> Publications > On Unit-Refutation Complete Formulae with Existentially Quantified Variables