Joshua Blinkhorn

Building Strategies into DQBF Proofs

VCLA hosted a talk by Joshua Blinkhorn

DATE:Tuesday, August 27, 2019
TIME:11:00 c.t.
VENUE:Library of the Algorithms and Complexity Group, HB 04 08 (Favoritenstrasse 9-11)


Quantified Boolean Formulas (QBF) are a natural extension of the SAT problem, with more sophisticated semantics: functions witnessing the truth of a QBF can be interpreted as strategies in a two-player game.

A lot has been written regarding the extraction of strategies from QBF proofs, in various proof systems. Here we devise a new system - Merge Resolution - in which strategies are built explicitly within the proofs themselves. We investigate some advantages of Merge Resolution over existing systems; in particular, we find that it lifts naturally to DQBF, a further extension of QBF. This is joint work with Olaf Beyersdorff and Meena Mahajan.


Joshua Blinkhorn, University of Leeds

Comments are closed.