SOQE 2021 The Second Workshop on Second-Order Quantifier Elimination and Related Topics Online Event, November 4, 2021 Associated with KR 2021, the 18th International Conference on Principles of Knowledge Representation and Reasoning, November 3–12, 2021 Proceedings Renate A. Schmidt · Christoph Wernhard · Yizheng Zhao (Eds.) Editors Renate A. Schmidt The University of Manchester Manchester UK Christoph Wernhard University of Potsdam Potsdam Germany Yizheng Zhao Nanjing University Nanjing China Copyright © 2021 for the individual papers by the papers’ authors. Copyright © 2021 for the volume as a collection by its editors. This volume and its papers are published under the Creative Commons License Attribution 4.0 International (CC BY 4.0). Preface This volume contains the papers presented at the Second Workshop on Second- order Quantifier Elimination and Related Topics (SOQE 2021) held on Novem- ber 4, 2021, due to the pandemic situation as an online event, associated with the 18th International Conference on Principles of Knowledge Representation and Reasoning (KR 2021). It continues the SOQE Workshop Series, which was initiated with SOQE 2017 in Dresden. 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 com- putation of definientia, the notion of conservative theory extension, abduction, notions of weakest sufficient and strongest necessary condition, and generaliza- tions of Boolean unification to predicate logic. It is attractive as a logic-based approach to various computational tasks, for example, the computation of cir- cumscription, 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 sim- plifications in reasoner preprocessing. Given the relevance of SOQE and related topics for various particular fields, our call for papers asked not just for novel contributions, but also for abstracts of pre-published work that so far was presented only in other contexts. We received 14 papers out which 12 were accepted for this volume, 5 as regular papers, 3 as short papers and 4 as abstracts of pre-published work. In addition to the contributed papers, the program included two invited talks by leading experts: – Frank Wolter on Living Without Beth and Craig: Explicit Definitions and Interpolants without Beth Definability and Craig Interpolation – David Toman on Projective Beth Definability and Craig Interpolation for Relational Query Optimization We would like to thank all those involved for their enthusiasm and high-quality contributions, in particular, the invited speakers, the authors of research papers, the members of the Program Committee, and the KR 2021 Workshop Chairs Markus Krötzsch and Yongmei Liu who provided excellent support. November 2021 Renate A. Schmidt Christoph Wernhard Yizheng Zhao Organization Program Committee Chairs and Organizers Renate A. Schmidt The University of Manchester, UK Christoph Wernhard University of Potsdam, Germany Yizheng Zhao Nanjing University, China Program Commitee Philippe Balbiani IRIT, CNRS, University of Toulouse, France Jieying Chen University of Oslo, Norway James Delgrande Simon Fraser University, Canada Silvio Ghilardi Università degli Studi di Milano, Italy Stefan Hetzl Technische Universität Wien, Austria Patrick Koopmann Technische Universität Dresden, Germany Andreas Nonnengart DFKI, Germany Vladislav Ryzhikov Birkbeck, University of London, UK Stefan Schlobach Vrije Universiteit Amsterdam, Netherlands Renate A. Schmidt The University of Manchester, UK Viorica Sofronie-Stokkermans Universität Koblenz-Landau, Germany Andrzej Szalas Uniwersytet Warzawski, Poland and Linköpings Universitet, Sweden Sophie Tourret Inria, France and Max Planck Institute for Informatics, Germany Kewen Wang Griffith University, Australia Christoph Wernhard University of Potsdam, Germany Yizheng Zhao Nanjing University, China Additional Reviewer Alessandro Gianola Contents Invited Talks Projective Beth Definability and Craig Interpolation for Relational Query Optimization (Material to Accompany Invited Talk) . . . . . . . . 1 David Toman and Grant Wedell Living Without Beth and Craig: Explicit Definitions and Interpolants without Beth Definability and Craig Interpolation (Abstract of Invited Talk) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 Frank Wolter Research Papers Resolution-Based Uniform Interpolation for Multi-Agent Modal Logic Kn 15 Ruba Alassaf, Renate A. Schmidt and Uli Sattler Second-Order Specifications and Quantifier Elimination for Consistent Query Answering in Databases (Abstract) . . . . . . . . . . . . . . . . . . 28 Leopoldo Bertossi On Testing Containedness Between Geometric Graph Classes using Second-order Quantifier Elimination and Hierarchical Reasoning (Short Paper) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 Lucas Böltz, Hannes Frey, Dennis Peuter and Viorica Sofronie-Stokkermans Abduction in EL via Translation to FOL . . . . . . . . . . . . . . . . . . 46 Fajar Haifani, Patrick Koopmann and Sophie Tourret An Abstract Fixed-Point Theorem for Horn Formula Equations (Abstract) 59 Stefan Hetzl and Johannes Kloibhofer Signature-Based ABox Abduction in ALC is Hard . . . . . . . . . . . . . 61 Patrick Koopmann SEH-PILoT: A System for Property-Directed Symbol Elimination – Work in Progress (Short Paper) . . . . . . . . . . . . . . . . . . . . . . . . . . . 75 Philipp Marohn and Viorica Sofronie-Stokkermans Symbol Elimination and Applications to Parametric Entailment Problems (Abstract) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 83 Dennis Peuter and Viorica Sofronie-Stokkermans The Yoneda Reduction of Polymorphic Types (Abstract) . . . . . . . . . 92 Paolo Pistone and Luca Tranchini VI Applying Second-Order Quantifier Elimination in Inspecting Gödel’s Ontological Proof . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 98 Christoph Wernhard Sahlqvist-type Correspondence Theory for Second-Order Propositional Modal Logic (Short Paper) . . . . . . . . . . . . . . . . . . . . . . . . . . 112 Zhiguang Zhao Metadata-based Term Selection for Modularization and Uniform Interpolation of OWL Ontologies . . . . . . . . . . . . . . . . . . . . . . . 122 Xinhao Zhu, Xuan Wu, Ruiqing Zhao, Yu Dong and Yizheng Zhao