6 - 8 December 2017, Workshop on Second-order Quantifier Elimination & Related Topics (SOQE 2017), Dresden, Germany
Second-order quantifier elimination (SOQE) means to compute from a given logic formula with quantifiers upon second-order objects such as predicates, an equivalent formula in which these quantified second-order objects do no longer occur. It can be combined with various underlying logics, including classical propositional and first-order logic as well as modal and description logics. In slight variations it is also known as forgetting, projection, predicate elimination and uniform interpolation. It is particularly attractive as a logic-based approach to various computational tasks.
The workshop aims at bringing together researchers working on SOQE and related topics. The hope is that issues shared by problems emerging from different special contexts will become apparent, interesting open research problems will be identified, and potential new applications as well as demands on implementations will become visible.
We invite submissions of works with original research, adaptions of relevant research published elsewhere, and discussions of research in progress, as well as suggestions for tutorials on topics of interest.