Second-or der quantifier elimination (SOQE) means to compute from a given logic formula with quantifiers upon second-order objects such as predicates, an equiva lent formula in which these quantified second-orde r objects do no longer occur. It can be combined w ith various underlying logics, including classical propositional and first-order logic as well as mo dal and description logics. In slight variations i t is also known as forgetting, projection, predica te elimination and uniform interpolation. It is pa rticularly attractive as a logic-based approach to various computational tasks.
\n\nThe work shop aims at bringing together researchers working on SOQE and related topics. The hope is that issu es shared by problems emerging from different spec ial contexts will become apparent, interesting ope n research problems will be identified, and potent ial new applications as well as demands on impleme ntations will become visible.
\nWe invite submissions of works with original re search, adaptions of relevant research published e lsewhere, and discussions of research in progress, as well as suggestions for tutorials on topics of interest.
\n