Workshop on Theory and Applications of Quantified Boolean Formulas

Siena, June 18-19, 2001

in connection with IJCAR 2001

Program Committee

U. Egly (TU Wien, Co-Chair)
R. Feldmann (Univ. Paderborn, Co-Chair)
I. Gent (Univ. St. Andrews)
D. Mitchell (SFU Burnaby)
J. Rintanen (Univ. Freiburg)
M. Schaerf (Univ. Rome)
H. Tompits (TU Wien, Co-Chair)
T. Walsh (Univ. York)

Call for papers

Postscript, ps.gz

Important dates

Submission deadline: March 24, 2001
Notification of acceptance: April 27, 2001
Final version due: May 13, 2001
Early registration: to be announced

Contact

For further information, send an e-mail to qbf2001@kr.tuwien.ac.at.

Topic

In the last few years, there is a considerable increase of interest in quantified boolean formulas (QBFs), i.e., propositional formulas with the additional possibility to quantify over propositional variables. Besides a growing number of investigations discussing theoretical issues concerning QBFs, the availability of several QBF-solvers stimulated also some practically motivated research. For instance, applications for solving planning problems or various nonmonotonic reasoning tasks based on encodings to QBFs have been proposed. Also, proof-theoretical investigations for some quantified non-classical logics have been performed, like, e.g., studying several kinds of quantified fuzzy logics.

The aim of this workshop is to bring together people who are interested in theoretical and practical aspects of quantified boolean formulas. Topics of interest include (but are not limited to)

- proof theory and calculi for QBFs;

- implementations of QBF solvers;

- benchmark generation and evaluation methodology;

- applications of QBFs, e.g., in knowledge representation, planning, formal verification, etc.;

- (boolean) quantification and non-classical logics.

Accepted Papers

M. Baaz, A. Ciabattoni, N. Preining, H. Veith: A Guide to Quantified Propositional Goedel Logic
M. Cadoli, A. Schaerf: Compiling Problem Specifications into SAT
D. Ding, H. Kleine Buening, X. Zhao: Minimal Falsity for QBF with Fixed Deficiency
U. Egly, V. Klotz, H. Tompits, S. Woltran: A Toolbox for Abduction: Preliminary Report
E. Giunchiglia, M. Narizzano, A. Tacchella: On the effectiveness of backjumping and trivial truth in quantified boolean formulas satisfiability
R. Letz: Advances in Decision Procedures for Quantified Boolean Formulas
R. Pliuskevicius: Simple Decision Procedure for a Fragment of QPTL
T. Polacik: Quantified Propositional Formulas, Intuitionistic Logic, and Cantor Space
J. Rintanen: Partial implicit unfolding in the Davis-Putnam procedure for quantified Boolean formulae

Workshop Program

Submission

Authors should send submissions of up to 10 pages in postscript format by e-mail to qbf2001@kr.tuwien.ac.at . The papers are required to be formatted according to the LNCS guidelines in A4 format. Informal proceedings will be available at the workshop and are provided by IJCAR.

Participation

Participation will be by invitation only. All authors of accepted papers and PC members will be invited. Other researchers who are interested in participating should send an e-mail to qbf2001@kr.tuwien.ac.at by May 13, 2001.

Note that all participants must register to IJCAR.

Hans Tompits

Last modified: Mon Feb 5 2001