School of Technology and Computer Science Seminars
Building strategies into QBF proofs
by Meena Mahajan (The Institute of Mathematical Sciences, Chennai)
Friday, February 15, 2019
from
to
(Asia/Kolkata)
at A-201 (STCS Seminar Room)
at A-201 (STCS Seminar Room)
Description |
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. Joint work with Olaf Beyersdorff and Joshua Blinkhorn. To appear in STACS 2019. |
Organised by | Prahladh Harsha |