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.
© 2024. All rights reserved.
