QUANTIFY 2014: July 18, 2014
QUANTIFY 2014 – First International Workshop on Quantification
News
- IMPORTANT NOTE: the first session (08:45-10:15) of the workshop is joint with the LaSh workshop and takes place in a different room than the other sessions. Please consider the program for further information.
- Registration is open: http://vsl2014.at/registration/
- The workshop program is available, including talk abstracts.
Talks
Invited Talks
- Konstantin Korovin: Instantiation-based reasoning, EPR encodings and all that
- Fahiem Bacchus: Algorithmic Paradigms for Solving QBF
- Uwe Egly: Quantifier handling in calculi for quantified Boolean formulas
- Gergely Kovásznai, Andreas Fröhlich and Armin Biere: EPR Encodings of Bit-Vector Problems Even With Quantifiers
- Christoph Wintersteiger: Efficiently Solving Quantified Bit-Vectors
- Nikolaj Bjorner: Quantifier Projection
Contributed Talks
- Michael Cashmore, Maria Fox and Enrico Giunchiglia: Encoding Reachability with Quantification
- Javier Álvez, Montserrat Hermo and Paqui Lucio: Projective Quantifier Elimination for Equational Constraint Solving
- Andrew Reynolds, Cesare Tinelli and Leonardo De Moura: Finding Conflicting Instances of Quantified Formulas in SMT
- Hubie Chen: Beyond Q-Resolution and Prenex Form: A Proof System for Quantified Constraint Satisfaction
Overview
Quantifiers play an important role in language extensions of many logics. The use of quantifiers
often allows for a more succinct encoding as it would be possible without quantifiers. However,
the introduction ofquantifiers affects the complexity of the extended formalism in general. In
consequence, theoretical results established for the quantifier-free formalism may not directly
be transferred to the quantified case. Further, techniques successfully implemented in reasoning
tools for quantifier-free formulas cannot directly be lifted to a quantified version.
The goal of the Workshop on Quantification (QUANTIFY 2014) is to bring together researchers
The goal of the Workshop on Quantification (QUANTIFY 2014) is to bring together researchers
who investigate the impact of quantification from a theoretical as well as from a practical point of
view. Quantification is a topic in different research areas, e.g., in SAT in terms of QBF, in CSP
in terms of QCSP, in SMT, etc. This workshop has the aim to provide an interdisciplinary
forum where researchers of various fields may exchange their experiences.
In particular, the following topics shall be considered at the workshop:
- Theoretical aspects of quantification
- Practical aspects of quantifications
- Intersections between the different research communities working on quantification
Call for Papers
http://vsl2014.at/pages/QUANTIFY-cfp.html
Organization
- Albert Atserias (Universitat Politecnica de Catalunya)
- Nikolaj Bjorner (Microsoft Research)
- Hubie Chen (Universidad del Pa\'{i}s Vasco and Ikerbasque) - chair
- Mikolas Janota (INESC-ID Lisboa)
- Hans Kleine Büning (University of Paderborn)
- Konstantin Korovin (Manchester University)
- Laura Kovacs (Chalmers University of Technology)
- Florian Lonsing (Vienna University of Technology) - chair
- Francesco Scarcello (DIMES, University of Calabria)
- Martina Seidl (Johannes Kepler University Linz) - chair
- Christoph M. Wintersteiger (Microsoft Research)