SOQE 2021
The 2nd Workshop on Second-Order Quantifier Elimination and Related Topics
Associated with KR 2021
4 November 2021

Aims and Topics Invited Talks Call for Papers Proceedings Registration Important Dates KR 2021 Program Program Committee Program Committee Chairs and Organizers

Aims and Topics

Second-order quantifier elimination (SOQE) is the problem of equivalently reducing a formula with quantifiers upon second-order objects such as predicates to a formula in which these quantified second-order objects no longer occur. In slight variations, SOQE is known as forgetting, projection, predicate elimination, and uniform interpolation. It can be combined with various underlying logics, including propositional, modal, description and first-order logics.

SOQE and its variations bear 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, and generalizations of Boolean unification to predicate logic. It is attractive as a logic-based approach to various computational tasks, for example, the computation of circumscription, the computation of modal correspondence properties, forgetting in knowledge bases, knowledge-base modularization, abductive reasoning and generating 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
• Historical aspects of SOQE
• Ontology modularization and content extraction
• Query processing and rewriting on the basis of definability
• Relationships between elimination and decidability
• Separability and inseparability

The workshop aims to bring together researchers working on SOQE and all these related topics to present, discuss and compare issues shared by problems emerging from different special contexts, interesting open research problems (perhaps with partial solutions), new applications, and implementation techniques.

The workshop is the second one in the Workshop on Second-Order Quantifier Elimination and Related Topics (SOQE) series, which was initiated with SOQE 2017 at TU Dresden.

Invited Talks

• David Toman, University of Waterloo, Canada Projective Beth Definability and Craig Interpolation for Relational Query Optimization
  Abstract: Accessing information using a high-level data model or ontology has been a long-standing objective of research communities in several areas. The underlying idea of separating a logical/conceptual view of how information is understood by users from a physical view of the layout of data in data structures – called (physical) data independence – has been a focus of research for more than fifty years. Here, we explore the issues connected with optimizing and executing relational queries and updates in this setting. In particular, we consider how to find appropriate reformulations of user queries over the physical design, and show how these ideas naturally relate to first-order definability and interpolation. The talk elaborates on how logic-based approaches can be used to capture both the high-level conceptual views of information and the low-level physical layout of data. Based on such a formalism, we present the design of a relational query optimizer based on Craig interpolation that allows users to compile both queries and updates to low-level code that operates directly over a physical encoding of the data. The ultimate objective of this design is to produce low-level code that performs comparably with hand-written code in low-level programming languages such as C.
• Frank Wolter, University of Liverpool, UK Living Without Beth and Craig: Explicit Definitions and Interpolants without Beth Definability and Craig Interpolation

  Abstract: In logics with the Craig interpolation property (CIP) the existence of an interpolant for an implication follows from the validity of the implication. In logics with the projective Beth definability property (PBDP), the existence of an explicit definition of a relation follows from the validity of a formula expressing its implicit definability. From an algorithmic viewpoint, the CIP and PBDP are of interest because they reduce existence problems to validity checking: an interpolant exists if, and only if, an implication is valid and an explicit definition exists if, and only if, a straightforward formula stating implicit definability is valid. The interpolant and explicit definition existence problems are thus not harder than validity.

  While many logics enjoy the CIP and the PBDP (for instance, first-order logic (FO), propositional logic, intuitionistic logic, and many modal and description logics), there are also many important logics that neither enjoy the CIP nor the PBDP. Examples include modal and description logics with nominals, the two-variable fragment of FO, the guarded fragment of FO, and most Horn-fragments of modal and description logics. In this talk, I will present recent results on the decidability and complexity of interpolant and explicit definition existence for logics that do not enjoy the CIP nor PBDP. For example, we show that the existence of explicit definitions of concept names (and individual names) relative to an ontology in the extension ALCO of ALC with nominals is 2ExpTime-complete and that the existence of explicit definitions of relation symbols in the guarded fragment is 3ExpTime-complete, thus in both case by one exponential harder than deduction. The presentation is based on the following joint work.

  • Alessandro Artale, Jean Christoph Jung, Andrea Mazzullo, Ana Ozaki, Frank Wolter: Living Without Beth and Craig: Definitions and Interpolants in Description Logics with Nominals and Role Inclusions. AAAI 2021: 6193–6201
  • Marie Fortin, Boris Konev, Frank Wolter: Interpolants and Explicit Definitions in Horn Description Logics (Extended Abstract). Description Logics 2021
  • Jean Christoph Jung, Frank Wolter: Living without Beth and Craig: Definitions and Interpolants in the Guarded and Two-Variable Fragments. LICS 2021: 1–14

Call for Papers

We invite submissions of high-quality research on variants of SOQE and related topics as well as submissions that describe applications, new systems or relevant data releases. Submissions will be reviewed by the program committee, which will select a balanced program of high-quality contributions.

Submissions can be one of the following type:

• Regular paper: up to 11 pages + bibliography
• Short paper: 5–6 pages + bibliography
• Abstract of pre-published paper: 1–6 pages + bibliography

Submissions should be written in English, formatted in the style of the Springer Publications format for Lecture Notes in Computer Science (LNCS). For details on the LNCS style, see Springer’s Author Instructions.

Papers should be submitted electronically via EasyChair at

• https://easychair.org/conferences/?conf=soqe2021

Regular papers must contain enough substance that they can be cited in other publications and may not have appeared before. Short papers may not have appeared before.

The complete call for papers in text format suitable for posting is available from here.

Proceedings

• Renate A. Schmidt, Christoph Wernhard, Yizheng Zhao (eds.):
  Proceedings of the Second Workshop on Second-Order Quantifier Elimination and Related Topics (SOQE 2021)
  Online Event, November 4, 2021
  CEUR Workshop Proceedings (CEUR-WS.org, ISSN 1613-0073)
  Volume 3009
  Aachen, 2021
  ONLINE: http://ceur-ws.org/Vol-3009/
  URN: urn:nbn:de:0074-3009-1
  BibTeX record

         @proceedings{soqe2021,
             booktitle = {Proceedings of the Second Workshop on Second-Order Quantifier Elimination and Related Topics (SOQE 2021)},
             year = {2021},
             editor = {Renate A. Schmidt and Christoph Wernhard and Yizheng Zhao},
             number = {3009},
             series = {CEUR Workshop Proceedings},
             address = {Aachen},
             issn = {1613-0073},
             url = {http://ceur-ws.org/Vol-3009},
             venue = {Virtual},
             eventdate = {2021-11-04},
         }
       

• All papers in a single PDF document

Registration

• Participants of SOQE 2021 have to register for KR 2021.
• It is expected that each submission is presented at the workshop by at least one of the authors, registered for KR 2021.
• Registration is free but mandatory. (The paper fee for KR 2021 does not apply to workshop papers, since these do not appear in the KR Proceedings.)

Important Dates

There will be two submission rounds. The first one is in sync with all the KR 2021 Workshops.

KR 2021

The workshop is organized as a satellite event of KR 2021, the 18th International Conference on Principles of Knowledge Representation and Reasoning, to be held fully online due to the pandemic situation on November 3–12, 2021.

The KR 2021 Workshops will take place in the period 3–5 November 2021.

Program

Thursday, 4 November 2021 (KR 2021, Room C)

Program Committee

Program Committee Chairs and Organizers