ICMS 2018 - Session 18: Quantifier Reasoning


Aim and Scope

The session aims at promoting discussion between researchers working on automated solving of problems involving quantifiers. Reasoning with quantifiers is intrinsically hard. Indeed, adding quantification to a theory typically leads to undecidability or to a much higher complexity class. However, quantifiers are extremely important in modeling real-world problems. In recent years there has been exciting progress in the research on quantifier reasoning. A number of novel solving paradigms can be found in various domains. Prime examples are quantified Boolean formulas (QBF) and satisfiability modulo theories (SMT). While quantifiers have similar semantics across different logics, the exchange between the different fields is limited. It is the objective of this session to bring together researchers tackling quantifiers from various angles. We believe that promoting such discussion enables mutual enrichment of the individual areas.

Topics (including, but not limited to)

Journal Special Issue

Accepted Talks

Leroy Chew: QBF Proof Systems Modulo NP

Konstantin Korovin and Josef Urban: First Experiments with Machine Learning of Useful Instantiations

Soonho Kong and Sicun Gao: Quantified Reasoning in dReal

Manuel Kauers and Martina Seidl: Symmetry Breaking for Solving Quantified Boolean Formulas

Haniel Barbosa: Towards higher-order unification in HOSMT

Mikolas Janota: On Machine Learning in Quantified Boolean Formulas

© 2021. All rights reserved.