Second-order quantifier elimination (SOQE) means to compute from a given logic formula with quantifiers upon second-order objects such as predicates an equivalent first-order formula, or, in other words, an equivalent formula in which these quantified second-order objects do no longer occur. It can be combined with various underlying logics, including classical propositional and first-order logic as well as modal and description logics. In slight variations it is also known as forgetting, projection, predicate elimination and uniform interpolation.
SOQE bears strong relationships to Craig interpolation, definability and computation of definientia, the notion of conservative theory extension, abduction and notions of weakest sufficient and strongest necessary condition, as well as to generalizations of Boolean unification to predicate logic. It is particularly attractive as a logic-based approach to various computational tasks, for example, the computation of circumscription, the computation of modal correspondences, forgetting in knowledge bases, knowledge-base modularization, computing abductive explanations, the specification of non-monotonic logic programming semantics, view-based query processing, and the characterization of formula simplifications in reasoner preprocessing.
Topics of interest include, but are not limited to:
The workshop aims at bringing together researchers working on SOQE and related topics. The hope is that issues shared by problems emerging from different special contexts will become apparent, interesting open research problems will be identified, and potential new applications as well as demands on implementations will become visible.
Tutorials aim to make foundations, methods and applications of SOQE and related techniques accessible to young researchers and to researchers with different specialist backgrounds.
We invite submissions of:
It is expected that submissions are presented at the workshop by at least one of the authors.
In general, the tutorials should take between 60 and 120 minutes.
Submissions should be written in English, formatted according to the Springer LNCS style, and match one of the following formats:
Submissions must be uploaded via EasyChair at:
Submissions will be reviewed by the PC, taking into account relevance, technical quality, quality of the presentation, and, as far as applicable, originality.
The complete call for papers and tutorials in text format suitable for posting is available from here.
Patrick Koopmann, Sebastian
Rudolph, Renate A. Schmidt, Christoph Wernhard (eds.):
Proceedings
of the Workshop on Second-Order Quantifier
Elimination and Related Topics (SOQE 2017)
Dresden, Germany, December 6-8, 2017
CEUR Workshop Proceedings (CEUR-WS.org, ISSN 1613-0073)
Volume 2013
Aachen, 2017
http://ceur-ws.org/Vol-2013/
Please register for participating at the workshop until 22 November 2017.
| 29 October 2017 | Abstract / Paper Submission | |
| 8 November 2017 | Author Notification | |
| 22 November 2017 | Camera-Ready Version for CEUR Proceedings | |
| 22 November 2017 | Registration | |
| 6-8 December 2017 | Workshop in Dresden |
The workshop will be located at
TU Dresden
Fakultät für Informatik (Andreas-Pfitzmann-Bau)
Nöthnitzer Straße 46
01187 Dresden
Room 2026
| Michael Benedikt | University of Oxford, UK | |
| Willem Conradie | University of Johannesburg, South Africa | |
| Boris Konev | University of Liverpool, UK | |
| Carsten Lutz | Universität Bremen, Germany | |
| Norbert Manthey | Software Consultant, Germany | |
| Andrzej Szałas | Uniwersytet Warzawski, Poland and Linköpings Universitet, Sweden | |
| Kewen Wang | Griffith University, Australia | |
| Yizheng Zhao | The University of Manchester, UK |
Thursday 7 December, starting in the late afternoon: Guided walk through Dresden's Old Town (brey kunst kultur), Dinner
On Friday 8 December the schedule will give opportunity to attend two invited talks of the QuantLA project as well as a Habilitation talk on topics of interest for the workshop:
| James Delgrande | Simon Fraser University, Canada | |
| Andreas Herzig | IRIT, France | |
| Stefan Hetzl | Technische Universität Wien, Austria | |
| Patrick Koopmann | TU Dresden, Germany | |
| Andreas Nonnengart | DFKI, Germany | |
| Hans Jürgen Ohlbach | Ludwig-Maximilians-Universität München, Germany | |
| Alessandra Palmigiano | TU Delft, Netherlands | |
| Sebastian Rudolph | TU 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 | TU Dresden, Germany | |
| Frank Wolter | University of Liverpool, UK | |
| Richard Zach | University of Calgary, Canada |
| Patrick Koopmann | TU Dresden, Germany | |
| Sebastian Rudolph | TU Dresden, Germany | |
| Renate A. Schmidt | The University of Manchester, UK | |
| Christoph Wernhard | TU Dresden, Germany |
Contact: info@christophwernhard.com