Second-or der quantifier elimination (SOQE) is the problem o f equivalently reducing a formula with quantifiers upon second-order objects such as predicates to a formula in which these quantified second-order ob jects no longer occur. In slight variations, SOQE is known as forgetting, projection, predicate elim ination, and uniform interpolation. It can be comb ined with various underlying logics, including pro positional, model, description and first-order log ics. It is attractive as a logic-based approach to various computational tasks.
\n\nThe work shop aims to bring together researchers working on SOQE and all these related topics to present, dis cuss and compare issues shared by problems emergin g from different special contexts, interesting ope n research problems (perhaps with partial solution s), new applications and implementation techniques . SOQE will be associated with the 18th Internatio nal Conference on Principles of Knowledge Represen tation and Reasoning (KR 2021).
\nWe invite submissions of high-quality researc h on variants of SOQE and related topics, includin g work that describes applications, new systems or relevant data releases. Submissions will be revie wed by the program committee, which will select a balanced program of high-quality contributions.
\n\nSubmissions can be one of the following
type:
\n Regular paper: up to 11 pages + bibli
ography Short paper: up to 5 pages + bibliography<
br>\n Both regular and short papers should be wri
tten in English, formatted in the style of the Spr
inger Publications format for Lecture Notes in Com
puter Science (LNCS).
\n Submissions must cont
ain enough substance that it they can be cited in
other publications and may not have appeared befor
e.