Editors Patrick Koopmann Technische Universitat Dresden Dresden Germany
Copyright c 2017 for the individual papers by the papers' authors. This volume is published and copyrighted by its editors. Second-order quanti er elimination (SOQE) is the problem of computing from a given logic formula involving quanti ers upon second-order objects such as predicates an equivalent rst-order formula, or, in other words, an equivalent formula in which these quanti ed second-order objects do no longer occur. The problem can be studied for various logics, including classical propositional and rst-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, de nability and computation of de nientia, the notion of conservative theory extension, abduction and notions of weakest su cient and strongest necessary condition, to correspondence theory relationships, as well as to generalizations of Boolean uni cation to predicate logic.
Various important research subjects of current interest are based on SOQE and these related notions, as is re ected in the topics addressed in workshop program: In the area of knowledge representation they include forgetting, uniform interpolation and abduction in description logics, modularization, reuse, versioning and summarization of ontologies, forgetting in variants of logic programming that are relevant for ontology reasoning, and query reformulation on the basis of interpolation. The uni ed 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 applications in the veri cation of distributed systems. The investigation of SOQE with respect to speci c fragments of rst-order logic is { much less researched than decidability { an area with open challenges, where, however, ways of progress can be indicated. For Boolean uni cation 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 identi ed 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 provides an exemplary framework for studying the dichotomy of expressivity versus complexity.
The rst Workshop on Second-order Quanti er Elimination and Related Topics (SOQE 2017) was held in the International Center for Computational Logic (ICCL) at Technische Universitat Dresden in Dresden, Germany, during 6-8 December 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 submissions of original research, adaptions of relevant research published elsewhere and discussions of research in progress.
We would like to thank all those involved for their enthusiasm and highquality 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 eld 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).
Organization SOQE 2017 was organized by the International Center for Computational Logic of Technische Universitat Dresden, Germany.
Andreas Herzig Stefan Hetzl Patrick Koopmann Andreas Nonnengart Hans Jurgen Ohlbach
Sebastian Rudolph Renate A. Schmidt Viorica Sofronie-Stokkermans David Toman Dirk Walther Christoph Wernhard Frank Wolter Richard Zach
Technische Universitat Dresden, Germany Technische Universitat Dresden, Germany The University of Manchester, UK Technische Universitat Dresden, Germany
IRIT, France Technische Universitat Wien, Austria Technische Universitat Dresden, Germany DFKI, Germany Ludwig-Maximilians-Universitat Munchen, Germany Technische Universiteit Delft, Netherlands Technische Universitat Dresden, Germany The University of Manchester, UK Universitat Koblenz-Landau, Germany University of Waterloo, Canada Fraunhofer IVI, Germany Technische Universitat Dresden, Germany University of Liverpool, UK University of Calgary, Canada
The workshop was supported by Deutsche Forschungsgemeinschaft (DFG) with grant WE 5641/1-1. Interpolation for Query Reformulation . . . . . . . . . . . . . . . . . . . .
Michael Benedikt Algorithmic Correspondence and Canonicity for Non-Classical Logics . . .
Willem Conradie Focusing on a Vocabulary: Ontology Inseparability, Uniform Interpolation and Modularity . . . . . . . . . . . . . . . . . . . . . . . . .
Boris Konev Conservative Extensions in Description Logics and Beyond . . . . . . . .
Carsten Lutz Elimination Techniques in Modern Propositional Logic Reasoning . . . .
Norbert Manthey Automated Forgetting and Uniform Interpolation: Three Tools . . . . . .
Renate A. Schmidt Swinging between Expressiveness and Complexity in Second-Order Formalisms: A Case Study . . . . . . . . . . . . . . . . . . . . . . . . . . .
Andrzej Szalas Forgetting for Logic Programs/Existential Rules . . . . . . . . . . . . . .
Kewen Wang (collaboration with Zhe Wang) Ackermann-Based Forgetting for Expressive Description Logics . . . . . .
Yizheng Zhao Resolution Based Uniform Interpolation and Forgetting for Expressive Description Logics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Patrick Koopmann Cut Elimination and Second Order Quanti er Elimination . . . . . . . . .
Alessandra Palmigiano 1 2 7 8 9 11 13 15 16 17 19
A Preliminary Comparison of the Forgetting Solutions Computed using SCAN, LETHE and FAME . . . . . . . . . . . . . . . . . . . . . . . . . .
Ruba Alassaf and Renate A. Schmidt Second Order Quanti er Elimination: Towards Veri cation Applications .
Silvio Ghilardi and Elena Pagani Towards Elimination of Second-Order Quanti ers in the Separated Fragment . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Marco Voigt VII 21 27 36 51 67 82 99 Early Steps of Second-Order Quanti er Elimination beyond the Monadic Case: The Correspondence between Heinrich Behmann and Wilhelm Ackermann 1928-1934 (Abstract) . . . . . . . . . . . . . . . . . . . . . . . 102
Christoph Wernhard