Local Soundness for QBF Calculi

EasyChair Preprint 362

Abstract

We develop new semantics for resolution-based calculi for Quantified Boolean Formulas, covering both the CDCL-derived calculi and the expansion-derived ones. The semantics is centred around the notion of a partial strategy for the universal player and allows us to show in a local, inference-by-inference manner that these calculi are sound. It also helps us understand some less intuitive concepts, such as the role of tautologies in long-distance resolution or the meaning of the ``star'' in the annotations of IRM. Furthermore, we show that a clause of any of these calculi can be, in the spirit of Curry-Howard correspondence, interpreted as a specification of the corresponding partial strategy. The strategy is total, i.e. winning, when specified by the empty clause.

Keyphrases: IRM-calc, QBF calculi, long-distance resolution, partial strategy, semantics, strategies, winning strategy

@booklet{EasyChair:362,
  author    = {Martin Suda and Bernhard Gleiss},
  title     = {Local Soundness for QBF Calculi},
  doi       = {10.29007/pkcj},
  howpublished = {EasyChair Preprint 362},
  year      = {EasyChair, 2018}}