SOQE 2017: Workshop on Second-Order Quantifier Elimination and Related Topics - Call for Papers and Tutorials

[Renate Schmidt]

[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 at christophwernhard.com

FUNDING

    The workshop is supported by Deutsche
    Forschungsgemeinschaft (DFG) with grant WE 5641/1-1.