VSL 2014: VIENNA SUMMER OF LOGIC 2014
QUANTIFY Home Page

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
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