Vol-3008⫷ Vol-3009 ⫸Vol-3010
urn:nbn:de:0074-3009-1

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 ) .

SOQE 2021
Second-Order Quantifier Elimination and Related Topics 2021

Proceedings of the Second Workshop on Second-Order Quantifier Elimination and Related Topics (SOQE 2021)
associated with the 18th International Conference on Principles of Knowledge Representation and Reasoning ( KR 2021 )

Online Event, November 4, 2021 .

Edited by

Renate A. Schmidt *
Christoph Wernhard
Yizheng Zhao *

* University of Manchester , UK
** University of Potsdam , Germany
*** Nanjing University , China

Table of Contents

Preface
Summary: There were 14 papers submitted for peer-review to this workshop. Out of these, 12 papers were accepted for this volume, 5 as regular papers, 3 as short papers and 4 as abstracts of pre-published work.

Invited Talks

Projective Beth Definability and Craig Interpolation for Relational Query Optimization (Material to Accompany Invited Talk) 1-13
David Toman , 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 K _n 15-27
Ruba Alassaf , Renate A. Schmidt , Uli Sattler
Second-Order Specifications and Quantifier Elimination for Consistent Query Answering in Databases (Abstract) 28-36
Leopoldo Bertossi
On Testing Containedness Between Geometric Graph Classes using Second-order Quantifier Elimination and Hierarchical Reasoning (Short Paper) 37-45
Lucas Böltz , Hannes Frey , Dennis Peuter , Viorica Sofronie-Stokkermans
Abduction in EL via Translation to FOL 46-58
Fajar Haifani , Patrick Koopmann , Sophie Tourret
An Abstract Fixed-Point Theorem for Horn Formula Equations (Abstract) 59-60
Stefan Hetzl , Johannes Kloibhofer
Signature-Based ABox Abduction in ALC is Hard 61-74
Patrick Koopmann
SEH-PILoT: A System for Property-Directed Symbol Elimination – Work in Progress (Short Paper) 75-82
Philipp Marohn , Viorica Sofronie-Stokkermans
Symbol Elimination and Applications to Parametric Entailment Problems (Abstract) 83-91
Dennis Peuter , Viorica Sofronie-Stokkermans
The Yoneda Reduction of Polymorphic Types (Abstract) 92-97
Paolo Pistone , Luca Tranchini
Applying Second-Order Quantifier Elimination in Inspecting Gödel's Ontological Proof 98-111
Christoph Wernhard
Sahlqvist-type Correspondence Theory for Second-Order Propositional Modal Logic (Short Paper) 112-121
Zhiguang Zhao
Metadata-based Term Selection for Modularization and Uniform Interpolation of OWL Ontologies 122-134
Xinhao Zhu , Xuan Wu , Ruiqing Zhao , Yu Dong Yizheng Zhao

2021-11-08: submitted by Christoph Wernhard, metadata incl. bibliographic data published under Creative Commons CC0
2021-11-14 : published on CEUR Workshop Proceedings (CEUR-WS.org, ISSN 1613-0073) | valid HTML5 |