BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Abandoning Prenex Clausal Normal Form in QBF Solving - Martina Sei
 dl -  Vienna University of Technology
DTSTART:20100318T110000Z
DTEND:20100318T120000Z
UID:TALK23712@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:*Abstract:* In the last decades\, numerous successful QSAT sol
 vers have been developed. However\, most of these solvers process formulas
  only in prenex conjunctive normal form (PCNF).  As for many practical app
 lications encodings into QBFs usually do not result in PCNF formulas\, a f
 urther transformation step is  necessary. This transformation often introd
 uces new variables and disrupts the structure of the formula.\nIn this tal
 k\, we discuss the disadvantages of prenex conjunctive normal form and des
 cribe an alternative way to process QBFs without the drawbacks of the norm
 al form transformation. We briefly describe the  solver qpro\, which is ab
 le to handle formulas in negation normal form. To this end\, we extend alg
 orithms for QBFs to the non-normal form case and generalize well-known pru
 ning concepts. For a concise description of the extended algorithms\, we f
 ollow a sequent-style characterization approach. \n\n*Biography:* Martina 
 Seidl is researcher at the Institute of Software Technology and Interactiv
 e Systems\, Vienna University of Technology\, Austria. She received her do
 ctoral degree in 2007 for the thesis “A Solver for Quantifi
 ed Boolean Formulas in Negation Normal Form`. Her research interests inclu
 de automated theorem proving with special focus on QBF solver construction
  and optimization techniques. Furthermore\, she is involved in research on
  model-driven engineering\, in particular on model versioning.
LOCATION:Small public lecture room\, Microsoft Research Ltd\, 7 J J Thomso
 n Avenue (Off Madingley Road)\, Cambridge
END:VEVENT
END:VCALENDAR