BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Microsoft Research Cambridge\, public talks
SUMMARY:Abandoning Prenex Clausal Normal Form in QBF Solvi
ng - Martina Seidl - Vienna University of Technol
ogy
DTSTART;TZID=Europe/London:20100318T110000
DTEND;TZID=Europe/London:20100318T120000
UID:TALK23712AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/23712
DESCRIPTION:*Abstract:* In the last decades\, numerous success
ful QSAT solvers have been developed. However\, mo
st of these solvers process formulas only in prene
x conjunctive normal form (PCNF). As for many pra
ctical applications encodings into QBFs usually do
not result in PCNF formulas\, a further transform
ation step is necessary. This transformation ofte
n introduces new variables and disrupts the struct
ure of the formula.\nIn this talk\, we discuss the
disadvantages of prenex conjunctive normal form a
nd describe an alternative way to process QBFs wit
hout the drawbacks of the normal form transformati
on. We briefly describe the solver qpro\, which i
s able to handle formulas in negation normal form.
To this end\, we extend algorithms for QBFs to th
e non-normal form case and generalize well-known p
runing concepts. For a concise description of the
extended algorithms\, we follow a sequent-style ch
aracterization approach. \n\n*Biography:* Martina
Seidl is researcher at the Institute of Software T
echnology and Interactive Systems\, Vienna Univers
ity of Technology\, Austria. She received her doct
oral degree in 2007 for the thesis Ã¢â‚¬Å“A Solver
for Quantified Boolean Formulas in Negation Norma
l Form`. Her research interests include automated
theorem proving with special focus on QBF solver c
onstruction and optimization techniques. Furthermo
re\, she is involved in research on model-driven e
ngineering\, in particular on model versioning.
LOCATION:Small public lecture room\, Microsoft Research Ltd
\, 7 J J Thomson Avenue (Off Madingley Road)\, Cam
bridge
CONTACT:Microsoft Research Cambridge Talks Admins
END:VEVENT
END:VCALENDAR