=Paper=
{{Paper
|id=Vol-2013/preface
|storemode=property
|title=None
|pdfUrl=https://ceur-ws.org/Vol-2013/preface.pdf
|volume=Vol-2013
}}
==None==
https://ceur-ws.org/Vol-2013/preface.pdf
SOQE 2017
Proceedings of the Workshop on
Second-Order Quantifier Elimination
and Related Topics,
Dresden, Germany,
December 6–8, 2017
Patrick Koopmann · Sebastian Rudolph ·
Renate A. Schmidt · Christoph Wernhard (Eds.)
Editors
Patrick Koopmann Sebastian Rudolph
Technische Universität Dresden Technische Universität Dresden
Dresden Dresden
Germany Germany
Renate A. Schmidt Christoph Wernhard
The University of Manchester Technische Universität Dresden
Manchester Dresden
UK Germany
Copyright c 2017 for the individual papers by the papers’ authors. This volume
is published and copyrighted by its editors.
Preface
Second-order quantifier elimination (SOQE) is the problem of computing from a
given logic formula involving quantifiers upon second-order objects such as pred-
icates an equivalent first-order formula, or, in other words, an equivalent formula
in which these quantified second-order objects do no longer occur. The problem
can be studied for various logics, including classical propositional and first-order
logic as well as modal and description logics. In slight variations SOQE is also
known as forgetting, projection, predicate elimination and uniform interpolation.
SOQE bears strong relationships to Craig interpolation, definability and com-
putation of definientia, the notion of conservative theory extension, abduction
and notions of weakest sufficient and strongest necessary condition, to correspon-
dence theory relationships, as well as to generalizations of Boolean unification
to predicate logic.
Various important research subjects of current interest are based on SOQE
and these related notions, as is reflected in the topics addressed in workshop
program: In the area of knowledge representation they include forgetting, uni-
form interpolation and abduction in description logics, modularization, reuse,
versioning and summarization of ontologies, forgetting in variants of logic pro-
gramming that are relevant for ontology reasoning, and query reformulation on
the basis of interpolation. The unified correspondence research program, which
recently emerged from the study of algorithmic correspondence and canonicity,
now by itself reaches into further areas such as proof theory. SOQE has applica-
tions in the verification of distributed systems. The investigation of SOQE with
respect to specific fragments of first-order logic is – much less researched than
decidability – an area with open challenges, where, however, ways of progress
can be indicated. For Boolean unification on the basis of predicate logic, like
SOQE an operation with formulas as output, various relationships to SOQE can
be shown. In the Algebra of Logic program of the 19th century SOQE was iden-
tified as an important operation, which makes the study of historical aspects
and the passage of SOQE to modern logic particularly interesting. Special forms
of SOQE are essential components of state-of-the-art SAT-solvers. SOQE pro-
vides an exemplary framework for studying the dichotomy of expressivity versus
complexity.
The first Workshop on Second-order Quantifier Elimination and Related Top-
ics (SOQE 2017) was held in the International Center for Computational Logic
(ICCL) at Technische Universität Dresden in Dresden, Germany, during 6-8 De-
cember 2017. The workshop aimed at bringing together researchers working on
SOQE and related topics in a dedicated event. Its program includes nine invited
talks, two tutorials and nine research talks, acquired with an open call for sub-
missions of original research, adaptions of relevant research published elsewhere
and discussions of research in progress.
IV
We would like to thank all those involved for their enthusiasm and high-
quality contributions, in particular, the invited speakers, the authors of tutorials
and research presentations, the members of the program committee, and Romy
Thieme who assisted with the local organization.
The organizational framework for the workshop was provided by the ICCL at
TU Dresden, an interdisciplinary center of competence in research and teaching
in the field of Computational Logic, with special emphasis on algebra, logic, and
formal methods in computer science, founded in 2003. The workshop was made
possible through funding by Deutsche Forschungsgemeinschaft (DFG) for the
project The Second-Order Approach and its Application to View-Based Query
Processing (grant WE 5641/1-1).
December 2017 Patrick Koopmann
Sebastian Rudolph
Renate A. Schmidt
Christoph Wernhard
Organization
SOQE 2017 was organized by the International Center for Computational Logic
of Technische Universität Dresden, Germany.
Program Chairs
Patrick Koopmann Technische Universität Dresden, Germany
Sebastian Rudolph Technische Universität Dresden, Germany
Renate A. Schmidt The University of Manchester, UK
Christoph Wernhard Technische Universität Dresden, Germany
Program Commitee
James Delgrande Simon Fraser University, Canada
Andreas Herzig IRIT, France
Stefan Hetzl Technische Universität Wien, Austria
Patrick Koopmann Technische Universität Dresden, Germany
Andreas Nonnengart DFKI, Germany
Hans Jürgen Ohlbach Ludwig-Maximilians-Universität München,
Germany
Alessandra Palmigiano Technische Universiteit Delft, Netherlands
Sebastian Rudolph Technische Universität Dresden, Germany
Renate A. Schmidt The University of Manchester, UK
Viorica Sofronie-Stokkermans Universität Koblenz-Landau, Germany
David Toman University of Waterloo, Canada
Dirk Walther Fraunhofer IVI, Germany
Christoph Wernhard Technische Universität Dresden, Germany
Frank Wolter University of Liverpool, UK
Richard Zach University of Calgary, Canada
Organization Chair
Christoph Wernhard Technische Universität Dresden, Germany
Funding
The workshop was supported by Deutsche Forschungsgemeinschaft (DFG) with
grant WE 5641/1-1.
Contents
Abstracts of Invited Talks
Interpolation for Query Reformulation . . . . . . . . . . . . . . . . . . . . 1
Michael Benedikt
Algorithmic Correspondence and Canonicity for Non-Classical Logics . . . 2
Willem Conradie
Focusing on a Vocabulary: Ontology Inseparability, Uniform
Interpolation and Modularity . . . . . . . . . . . . . . . . . . . . . . . . . 7
Boris Konev
Conservative Extensions in Description Logics and Beyond . . . . . . . . 8
Carsten Lutz
Elimination Techniques in Modern Propositional Logic Reasoning . . . . 9
Norbert Manthey
Automated Forgetting and Uniform Interpolation: Three Tools . . . . . . 11
Renate A. Schmidt
Swinging between Expressiveness and Complexity in Second-Order
Formalisms: A Case Study . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
Andrzej Szalas
Forgetting for Logic Programs/Existential Rules . . . . . . . . . . . . . . 15
Kewen Wang (collaboration with Zhe Wang)
Ackermann-Based Forgetting for Expressive Description Logics . . . . . . 16
Yizheng Zhao
Abstracts of Tutorials
Resolution Based Uniform Interpolation and Forgetting for Expressive
Description Logics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
Patrick Koopmann
Cut Elimination and Second Order Quantifier Elimination . . . . . . . . . 19
Alessandra Palmigiano
VII
Research Presentations
A Preliminary Comparison of the Forgetting Solutions Computed using
SCAN, LETHE and FAME . . . . . . . . . . . . . . . . . . . . . . . . . . 21
Ruba Alassaf and Renate A. Schmidt
Forgetting-Based Abduction in ALC-Ontologies (Extended Abstract) . . . 27
Warren Del-Pinto and Renate A. Schmidt
Second Order Quantifier Elimination: Towards Verification Applications . 36
Silvio Ghilardi and Elena Pagani
Computing ALCH-Subsumption Modules Using Uniform Interpolation . . 51
Patrick Koopmann and Jieying Chen
Towards Elimination of Second-Order Quantifiers in the Separated
Fragment . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67
Marco Voigt
Approximating Resultants of Existential Second-Order Quantifier
Elimination upon Universal Relational First-Order Formulas . . . . . . . 82
Christoph Wernhard
The Boolean Solution Problem from the Perspective of Predicate Logic
(Abstract) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 99
Christoph Wernhard
Early Steps of Second-Order Quantifier Elimination beyond the Monadic
Case: The Correspondence between Heinrich Behmann and Wilhelm
Ackermann 1928-1934 (Abstract) . . . . . . . . . . . . . . . . . . . . . . . 102
Christoph Wernhard
Algorithmic Correspondence and Canonicity for Possibility Semantics
(Abstract) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 106
Zhiguang Zhao