Martina Seidl: The QRAT proof system
Tid: On 2017-01-18 kl 12.00
Plats: Room 1537, Lindstedtsvägen 3, KTH
Medverkande: Martina Seidl, Johannes Kepler University Linz
PRACTICALITIES: Lunch is served at 12:00 noon (register at this doodle at the latest on Monday January 16, but preferably earlier). The presentation starts at 12:10 pm and ends at 1 pm. Those of us who wish reconvene after a short break for \(1\frac{1}{2}\)-2 hours of more technical discussions.
ABSTRACT
We present QRAT, a novel proof system for quantified Boolean formulas. With QRAT it is now possible to produce certificates for all reasoning techniques implemented in state-of-the-art QBF preprocessors. Such certificates are not only useful to efficiently validate the correctness of a result, but they also allow the extraction of Skolem functions, i.e., winning strategies for satisfiable formula instances.
In this talk, we first introduce the rules of QRAT, then we show how they can be used to express some powerful reasoning techniques implemented in modern preprocessors, and finally we outline how to extract a Skolem function from a QRAT proof.