SOQE 2021
The 2nd Workshop on Second-Order Quantifier Elimination and Related Topics
Associated with KR 2021
4 November 2021

Aims and Topics Invited Talks Call for Papers Proceedings Registration Important Dates KR 2021 Program Program Committee Program Committee Chairs and Organizers

Aims and Topics

Second-order quantifier elimination (SOQE) is the problem of equivalently reducing a formula with quantifiers upon second-order objects such as predicates to a formula in which these quantified second-order objects no longer occur. In slight variations, SOQE is known as forgetting, projection, predicate elimination, and uniform interpolation. It can be combined with various underlying logics, including propositional, modal, description and first-order logics.

SOQE and its variations bear strong relationships to Craig interpolation, definability and computation of definientia, the notion of conservative theory extension, abduction and notions of weakest sufficient and strongest necessary condition, and generalizations of Boolean unification to predicate logic. It is attractive as a logic-based approach to various computational tasks, for example, the computation of circumscription, the computation of modal correspondence properties, forgetting in knowledge bases, knowledge-base modularization, abductive reasoning and generating explanations, the specification of non-monotonic logic programming semantics, view-based query processing, and the characterization of formula simplifications in reasoner preprocessing.

Topics of interest include, but are not limited to:

The workshop aims to bring together researchers working on SOQE and all these related topics to present, discuss and compare issues shared by problems emerging from different special contexts, interesting open research problems (perhaps with partial solutions), new applications, and implementation techniques.

The workshop is the second one in the Workshop on Second-Order Quantifier Elimination and Related Topics (SOQE) series, which was initiated with SOQE 2017 at TU Dresden.

Invited Talks

Call for Papers

We invite submissions of high-quality research on variants of SOQE and related topics as well as submissions that describe applications, new systems or relevant data releases. Submissions will be reviewed by the program committee, which will select a balanced program of high-quality contributions.

Submissions can be one of the following type:

Submissions should be written in English, formatted in the style of the Springer Publications format for Lecture Notes in Computer Science (LNCS). For details on the LNCS style, see Springer’s Author Instructions.

Papers should be submitted electronically via EasyChair at

Regular papers must contain enough substance that they can be cited in other publications and may not have appeared before. Short papers may not have appeared before.

The complete call for papers in text format suitable for posting is available from here.



Important Dates

There will be two submission rounds. The first one is in sync with all the KR 2021 Workshops.

2 July 2021 Extended to 23 July 2021 Paper Submission (1st Round)
6 August 2021 27 August 2021 Author Notification (1st Round)
9 September 2021 Extended to 16 September 2021 Paper Submission (2nd Round)
7 October 2021 Author Notification (2nd Round)
15 October 2021 Registration with the host conference KR 2021
21 October 2021 Camera-Ready Version due
4 November 2021 SOQE Workshop (10:00–18:30 CET)

KR 2021

The workshop is organized as a satellite event of KR 2021, the 18th International Conference on Principles of Knowledge Representation and Reasoning, to be held fully online due to the pandemic situation on November 3–12, 2021.

The KR 2021 Workshops will take place in the period 3–5 November 2021.


Thursday, 4 November 2021 (KR 2021, Room C)

10:00 – 10:05 CET Opening Renate A. Schmidt, Christoph Wernhard, Yizheng Zhao
10:05 – 11:05 CET Invited Talk Chair: Renate A. Schmidt
Frank Wolter
Living Without Beth and Craig: Explicit Definitions and Interpolants without Beth Definability and Craig Interpolation
11:05 – 11:45 CET Contributed Talks Chair: Andrzej Szałas
11:05 – 11:25 CET Stefan Hetzl and Johannes Kloibhofer
An Abstract Fixed-Point Theorem for Horn Formula Equations
11:25 – 11:45 CET Paolo Pistone and Luca Tranchini
The Yoneda Reduction of Polymorphic Types
11:45 – 12:10 CET Coffee Break
12:10 – 13:30 CET Contributed Talks Chair: Viorica Sofronie-Stokkermans
12:10 – 12:30 CETPatrick Koopmann
Signature-Based ABox Abduction in ALC is Hard
12:30 – 12:50 CET Fajar Haifani, Patrick Koopmann and Sophie Tourret
Abduction in EL via Translation to FOL
12:50 – 13:10 CETXinhao Zhu, Xuan Wu, Ruiqing Zhao, Yu Dong and Yizheng Zhao
Metadata-based Term Selection for Modularization and Uniform Interpolation of OWL Ontologies
13:10 – 13:30 CET Leopoldo Bertossi
Second-Order Specifications and Quantifier Elimination for Consistent Query Answering in Databases
13:30 – 15:00 CET Lunch Break
15:00 – 16:00 CET Invited Talk Chair: Patrick Koopmann
David Toman
Projective Beth Definability and Craig Interpolation for Relational Query Optimization
16:00 – 16:40 CET Contributed Talks Chair: Patrick Koopmann
16:00 – 16:20 CETRuba Alassaf, Renate A. Schmidt and Uli Sattler
Resolution-Based Uniform Interpolation for Multi-Agent Modal Logic Kn
16:20 – 16:40 CET Zhiguang Zhao
Sahlqvist-type Correspondence Theory for Second-Order Propositional Modal Logic
16:40 – 17:10 CET Coffee Break
17:10 – 18:30 CET Contributed Talks Chair: Andreas Nonnengart
17:10 – 17:30 CET Christoph Wernhard
Applying Second-Order Quantifier Elimination in Inspecting Gödel's Ontological Proof
17:30 – 17:50 CET Dennis Peuter and Viorica Sofronie-Stokkermans
Symbol Elimination and Applications to Parametric Entailment Problems
17:50 – 18:10 CET Lucas Böltz, Hannes Frey, Dennis Peuter and Viorica Sofronie-Stokkermans
On Testing Containedness Between Geometric Graph Classes using Second-order Quantifier Elimination and Hierarchical Reasoning
18:10 – 18:30 CET Philipp Marohn and Viorica Sofronie-Stokkermans
SEH-PILoT: A System for Property-Directed Symbol Elimination

Program Committee

Philippe Balbiani IRIT, CNRS, University of Toulouse, France
Jieying Chen University of Oslo, Norway
James DelgrandeSimon Fraser University, Canada
Silvio GhilardiUniversità degli Studi di Milano, Italy
Stefan HetzlTechnische Universität Wien, Austria
Patrick Koopmann Technische Universität Dresden, Germany
Andreas Nonnengart DFKI, Germany
Vladislav Ryzhikov Birkbeck, University of London, UK
Stefan SchlobachVrije Universiteit Amsterdam, Netherlands
Renate A. Schmidt The University of Manchester, UK
Viorica Sofronie-Stokkermans Universität Koblenz-Landau, Germany
Andrzej SzałasUniwersytet Warzawski, Poland and Linköpings Universitet, Sweden
Sophie TourretInria, France and Max Planck Institute for Informatics, Germany
Kewen WangGriffith University, Australia
Christoph Wernhard University of Potsdam, Germany
Yizheng Zhao Nanjing University, People's Republic of China

Program Committee Chairs and Organizers

Renate A. Schmidt The University of Manchester, UK
Christoph Wernhard University of Potsdam, Germany
Yizheng Zhao Nanjing University, People's Republic of China

Aims and Topics Call for Papers Proceedings Registration Important Dates KR 2021 Invited Talks Program Program Committee Program Committee Chairs and Organizers