SOQE 2017
Workshop on Second-Order Quantifier Elimination
and Related Topics
TU Dresden, Germany, 6-8 December 2017

Aims and Topics Call for Papers and Tutorials Proceedings Registration Important Dates Venue Invited Speakers Program Program Committee Program Committee Chairs Organization Funding

Aims and Topics

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.

Call for Papers and Tutorials

We invite submissions of:

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.

Proceedings

Proceedings of the workshop will be published as CEUR workshop proceedings.

Registration

Please register for participating at the workshop until 22 November 2017.

Important Dates

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

Venue

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

Invited Speakers

Michael Benedikt University of Oxford, UK
Willem Conradie University of Johannesburg, South Africa
Boris KonevUniversity of Liverpool, UK
Carsten LutzUniversität Bremen, Germany
Norbert MantheySoftware Consultant, Germany
Andrzej SzałasUniwersytet Warzawski, Poland and Linköpings Universitet, Sweden
Kewen WangGriffith University, Australia
Yizheng ZhaoThe University of Manchester, UK

Program

The workshop will start on Wednesday 6 December at 9 AM and last until Friday 8 December late afternoon.

Invited Talks

Tutorials

Research Talks

Excursion

Program Committee

James DelgrandeSimon Fraser University, Canada
Andreas HerzigIRIT, France
Stefan HetzlTechnische 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 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

Program Committee Chairs

Patrick Koopmann TU Dresden, Germany
Sebastian Rudolph TU Dresden, Germany
Renate Schmidt The University of Manchester, UK
Christoph Wernhard TU Dresden, Germany

Organization

Christoph Wernhard, TU Dresden – International Center for Computational Logic, info@christophwernhard.com

Funding

The workshop is supported by Deutsche Forschungsgemeinschaft (DFG) with grant WE 5641/1-1.
Aims and Topics Call for Papers and Tutorials Proceedings Registration Important Dates Venue Invited Speakers Program Program Committee Program Committee Chairs Organization Funding

Contact: info@christophwernhard.com