Marco Benedetti

Title: Anatomy and Usage of Certificates for Quantified Formulas

Abstract: Certificates for Quantified Boolean Formulas (QBF) and related
formalisms (such as QCSP, Quantified Constraint Satisfaction Problems)
are compact structures meant to ensure the validity of a formula in a
solver-independent and deduction-free way. In this talk, we first discuss
how QBF certificates can be represented, verified, and constructed.  Then,
we examine their hidden potential in tasks other than a mere verification
of validity. We provide historical notes on the subject, discussing why
they have been proposed in the first place, how they have been used so
far, and which real-world applications are likely to benefit from them
in the future. Illustrative examples and some challenging applications
are also covered.