In conjunction with IJCAR 2024.

News:

  • Program is online

  • Deadline extension

Program

14:30

Manuel Kauers

Symmetries of Quantified Boolean Formulas

[SAT paper]

15:30

Jørgen Villadsen and Roberto Pettinau

Formalizing Implicational Axiomatics for Classical First-Order Logic with Functions in Isabelle/HOL

[Extended abstract]

16:00

Break

16:30

Adrian Rebola Pardo

Boolean Quantifier Shifting as an Optimization Problem

[Ressources]

17:00

Sibylle Möhle

Enumerative Solution Counting for QBFs

[CP paper, CICM paper, slides]

17:30

Maximilian Heisinger

The Logic Shell

[Ressources]

18:00

Discussion

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 of quantifiers 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 2024) 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

Topics

The workshop is concerned with all theoretical and practical aspects of quantification in logics such as QBF, QCSP, SMT, and theorem proving. The topics of interest include (but are not limited to):

  • Complexity results

  • Encodings with and without quantification and comparisons thereof

  • Applications of quantification

  • Implementations of reasoning tools

  • Case studies and experimental results

  • Intersections between the different research communities working on quantification

  • Surveys of state-of-the-art approaches to handling quantification

Submission

Submissions of extended abstracts, full papers, and tutorials are solicited and will be managed via Easychair:

Submitted papers should be formatted in LNCS format.

We solicit three types of submissions:

  • Talk abstracts (maximum two pages, excluding references) describing already published results.

  • Full papers (maximum 15 pages, excluding references) on novel, unpublished work.

  • Tutorial papers (maximum 15 pages, excluding references) introducing a research field related to quantifiers.

The talk abstracts should include a relevant bibliography of related work and an outline of the planned talk. For this category, we explicitly advocate talks which summarize the results of one or more already published papers.

Full papers should contain novel, unpublished work that qualifies to be published in a special issue of a journal or formal workshop proceedings. The 15 pages are an upper limit, shorter papers are also welcome.

Tutorial papers should survey results already published, maybe in multiple articles or presentations capturing the commonalities and differences of various quantification approaches (perhaps even interdisciplinary).

Each submission will be assessed by the program committee and the workshop organizers with respect to novelty, originality, and scope.

Submissions related to completed work as well as work in progress are welcome. Authors are encouraged to provide additional material such as source code of tools, experimental data, benchmarks and related publications in an appendix or a related webpage. The additional material will be considered at the discretion of the reviewers.

Previously published work or extensions thereof may be submitted to the workshop but that case has to be explicitly stated in the submitted paper. This regulation also applies to work which is currently under review elsewhere.

Authors of accepted abstracts and papers are expected to give a talk at the workshop.

The outcomes of the discussions will be summarized in a workshop report, which can be made publicly available as technical report (unless the participants decide not to do so).

In case we get enough full and tutorial papers, we will organize a special issue on quantification (e.g., in the Journal of Satisfiability (JSAT) or formal workshop proceedings.

Program Committee

  • Konstantin Korovin, University of Manchester

  • Martina Seidl, Johannes Kepler University Linz

  • Stephan Schulz, DHBW Stuttgart

  • Geoff Sutcliffe, University of Miami

  • Friedrich Slivovsky, University of Liverpool

  • Alberto Griggio, Fondazione Bruno Kessler

  • Hubie Chen, King’s College London

  • Erika Abraham, RWTH Aachen University

  • Pascal Fontaine, Université de Liège

Important Dates

  • Round 1 (notification before early registration deadline)

    • Submission: May 25 for talk abstracts, May 15 for all other paper categories

    • Notification: May 30

  • Round 2 (notification after early registration deadline)

    • Submission: June 10 (talk abstracts only!!!)

    • Notification: June 15

  • Workshop: July 1

Contact