| 9:20-9:30 | Welcome and Introductory Remarks |
| Session 1: | Applications |
| 9:30-10:00 | Compiling Problem Specifications into SAT |
| M. Cadoli, A. Schaerf | |
| 10:00-10:30 | A Toolbox for Abduction: Preliminary Report |
| U. Egly, V. Klotz, H. Tompits, S. Woltran | |
| 10:30-11:00 | Coffee Break |
| Session 2: | Systems and Procedures for QBFs |
| 11:00-11:30 | On the effectiveness of backjumping and trivial truth in quantified boolean formulas satisfiability |
| E. Giunchiglia, M. Narizzano, A. Tacchella | |
| 11:30-12:00 | Advances in Decision Procedures for Quantified Boolean Formulas |
| R. Letz | |
| 12:00-12:30 | Minimal Falsity for QBF with Fixed Deficiency |
| Decheng Ding, H. Kleine Buening, Xishun Zhao | |
| 12:30-14:00 | Lunch Break |
| Session 3: | QBFs and Non-classical Logics |
| 14:00-14:30 | A Guide to Quantified Propositional Goedel Logic |
| M. Baaz, A. Ciabattoni, N. Preining, H. Veith | |
| 14:30-15:00 | Simple Decision Procedure for a Fragment of QPTL |
| R. Pliuskevicius | |
| 15:00-15:30 | Quantified Propositional Formulas, Intuitionistic Logic, and Cantor Space |
| T. Polacik | |
| 15:30-16:00 | Coffee Break |
| Session 4: | Methods |
| 16:00-16:30 | TBA |
| A. Voronkov | |
| 16:30-17:00 | Partial implicit unfolding in the Davis-Putnam procedure for quantified Boolean formulae |
| J. Rintanen |