[Apologies if you receive multiple copies. Please forward 
this call to interested parties.]

               CALL FOR PAPERS AND TUTORIALS

                         SOQE 2017
      WORKSHOP ON SECOND-ORDER QUANTIFIER ELIMINATION
                     AND RELATED TOPICS

                    TU Dresden, Germany
                     6-8 December 2017

                 Deadline: 29 October 2017

                   http://2017.soqe.org/

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:

   * Abduction
   * Access interpolation
   * Algorithms for SOQE and related tasks
   * Applications of SOQE and related techniques
   * Automation and tools
   * Boolean equation solving / Boolean unification and SOQE
   * Characterizations of formula classes on which SOQE succeeds
   * Circumscription
   * Conservative theory extensions
   * Craig interpolation
   * Definability and computation of definienda
   * Elimination in formula simplifications
   * Elimination methods and calculi for theorem proving
   * Forgetting and projection in answer set programming
   * Forgetting and uniform interpolation in description logics
   * Historical aspects of SOQE
   * Ontology modularization
   * Relationships between elimination and decidability
   * View-based query rewriting on the basis of definability

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

   We invite submissions of:

   * Works with original research, adaptions of relevant
     research published elsewhere, and discussions of
     research in progress.

     It is expected that submissions are presented at the
     workshop by at least one of the authors.

   * Suggestions for tutorials on topics of interest.

     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:

   * Full research paper: up to 15 pages + bibliography
   * Extended abstract: 5-8 pages + bibliography
   * Abstract: 1-4 pages
   * Tutorial abstract: 1-5 pages.

   Submissions must be uploaded via EasyChair at:
   https://easychair.org/conferences/?conf=soqe2017

   Submissions will be reviewed by the PC, taking into
   account relevance, technical quality, quality of the
   presentation, and, as far as applicable, originality.

PROCEEDINGS

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

REGISTRATION
   
   Details will be announced on the workshop webpage. No fee
   will be charged for attending the workshop.

IMPORTANT DATES

   29 October 2017:    Abstract / Paper Submission
   8 November 2017:    Author Notification
   22 November 2017:   Registration
   22 November 2017:   Camera-Ready Version for CEUR
   6-8 December 2017:  Workshop in Dresden

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.