Proceedings Renate A. Schmidt The University of Manchester Manchester UK Christoph Wernhard University of Potsdam Potsdam Germany 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). This volume contains the papers presented at the Second Workshop on Secondorder Quanti er Elimination and Related Topics (SOQE 2021) held on November 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 quanti er elimination (SOQE) is the problem of equivalently reducing a formula with quanti ers upon second-order objects such as predicates to a formula in which these quanti ed 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 rst-order logics. SOQE and its variations bear strong relationships to Craig interpolation, de nability and computation of de nientia, the notion of conservative theory extension, abduction, notions of weakest su cient and strongest necessary condition, and generalizations of Boolean uni cation 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 speci cation of non-monotonic logic programming semantics, view-based query processing, and the characterization of formula simpli cations in reasoner preprocessing.
Given the relevance of SOQE and related topics for various particular elds, 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 De nitions and
Interpolants without Beth De nability and Craig Interpolation { David Toman on Projective Beth De nability 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 Krotzsch and Yongmei Liu who provided excellent support.
Renate A. Schmidt Christoph Wernhard Yizheng Zhao
Philippe Balbiani Jieying Chen James Delgrande Silvio Ghilardi Stefan Hetzl Patrick Koopmann Andreas Nonnengart Vladislav Ryzhikov Stefan Schlobach Renate A. Schmidt Viorica Sofronie-Stokkermans Andrzej Szalas Sophie Tourret Kewen Wang Christoph Wernhard Yizheng Zhao
Alessandro Gianola
University of Potsdam, Germany Nanjing University, China IRIT, CNRS, University of Toulouse, France University of Oslo, Norway Simon Fraser University, Canada Universita degli Studi di Milano, Italy Technische Universitat Wien, Austria Technische Universitat Dresden, Germany DFKI, Germany Birkbeck, University of London, UK Vrije Universiteit Amsterdam, Netherlands The University of Manchester, UK Universitat Koblenz-Landau, Germany Uniwersytet Warzawski, Poland and
Linkopings Universitet, Sweden Inria, France and Max Planck Institute for
Informatics, Germany Gri th University, Australia University of Potsdam, Germany
Nanjing University, China
Projective Beth De nability and Craig Interpolation for Relational Query Optimization (Material to Accompany Invited Talk) . . . . . . . .
David Toman and Grant Wedell Living Without Beth and Craig: Explicit De nitions and Interpolants without Beth De nability and Craig Interpolation (Abstract of Invited Talk) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Frank Wolter
Resolution-Based Uniform Interpolation for Multi-Agent Modal Logic Kn
Ruba Alassaf, Renate A. Schmidt and Uli Sattler Second-Order Speci cations and Quanti er Elimination for Consistent Query Answering in Databases (Abstract) . . . . . . . . . . . . . . . . . .
Leopoldo Bertossi On Testing Containedness Between Geometric Graph Classes using Second-order Quanti er Elimination and Hierarchical Reasoning (Short Paper) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Lucas Boltz, Hannes Frey, Dennis Peuter and Viorica
Sofronie-Stokkermans Abduction in E L via Translation to FOL . . . . . . . . . . . . . . . . . .
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 . . . . . . . . . . . . .
Patrick Koopmann SEH-PILoT: A System for Property-Directed Symbol Elimination { Work in Progress (Short Paper) . . . . . . . . . . . . . . . . . . . . . . . . . . .
Philipp Marohn and Viorica Sofronie-Stokkermans Symbol Elimination and Applications to Parametric Entailment Problems (Abstract) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Dennis Peuter and Viorica Sofronie-Stokkermans The Yoneda Reduction of Polymorphic Types (Abstract) . . . . . . . . .
Paolo Pistone and Luca Tranchini 1 14 15 28 37 46 61 75 83 92 Applying Second-Order Quanti er Elimination in Inspecting Godel's Ontological Proof . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 98
Christoph Wernhard