https://www.dagstuhl.de/20191

03. – 08. Mai 2020, Dagstuhl-Seminar 20191

Extending the Synergies Between SAT and Description Logics

Organisatoren

Joao Marques-Silva (University of Lisbon, PT)
Rafael Penaloza (University of Milano-Bicocca, IT)
Uli Sattler (University of Manchester, GB)

Auskunft zu diesem Dagstuhl-Seminar erteilen

Susanne Bach-Bernhard zu administrativen Fragen

Michael Gerke zu wissenschaftlichen Fragen

Motivation

Propositional satisfiability (SAT) and Description Logics (DL) are two successful areas of computational logic where automated reasoning plays a fundamental role. At an abstract level, they can all be considered part of the same family of logical formalisms, which can be used to represent knowledge of a domain, with their main difference being the expressivity of the formalism and the complexity of reasoning. Despite their similarities in intent and scope, SAT and DLs have evolved via different routes. While the DL community focused on understanding the precise computational complexity of reasoning in the different fragments it studies, the SAT community was building highly optimised solvers capable of dealing with industrial-size problems, and later adapting their techniques to variants of satisfiability. Although there have been attempts to produce highly efficient reasoners for DLs as well, dealing with problems that go beyond standard reasoning remains a challenge in this field.

This Dagstuhl Seminar will bring together researchers from the SAT and DL communities viewed in a wide sense, to discuss potential collaborations and develop deeper synergies between them, discovering how these communities can contribute to each other. Specifically, we intend to discuss which DL reasoning problems can be efficiently solved or optimised with the help of SAT techniques and tools, and how can the SAT community benefit from this cross-fertilisation. In the end, we will map a plan for new theoretical, technical, and industrial developments that are considered relevant from the discussions in the Seminar. Some of the open problems to be discussed are the theoretical extension of SAT-developed methods to handle reasoning in more expressive logics, and the practical aspect of designing and using adequate data structures for efficient implementations. Taking into account the expertise of the participants, and recent efforts in these directions, we will encourage discussions on standardisation and system connectivity.

Existing preliminary work has already shown the benefits of applying SAT-based methods for solving non-standard problems in DLs, but the topic needs a more thorough analysis. Indeed, it becomes increasingly clear that the DL and SAT communities have much to offer to each other with some potentially deep connections and advanced applications. However, a major obstacle is the lack of communication and (by extension) collaboration between the fields. Bridging the communities requires a common understanding of the vocabulary, problems, and goals that each aims for. Only then can the two areas construct a synergy for mutual growth and development.

This seminar is based on the idea that understanding is fundamental for collaboration and cooperation. After explaining the common grounds, we will try to answer how DLs and SAT can benefit each other. On the one hand, the experience of building industrial-strength tools can help the development of new DL reasoners. On the other hand, DL-based problems may provide new challenges for the SAT community to tackle. By bringing experts from both fields, we expect to spark discussions that lead to a closer relationship between them, and future collaborations at different levels. The Seminar is conceived as a seed for fruitful collaborations, leading to the identification of new research topics, building of consortia, and applications to research funds.

During the seminar, the participants will engage in various focus groups so that we can elicit different perspectives on a number of topics. We will also include a series of plenary talks complemented by breakout and coordination sessions focusing on specific issues. The program will include ample opportunities for one-on-one discussions and other social interactions.

License
  Creative Commons BY 3.0 DE
  Joao Marques-Silva, Rafael Penaloza, and Uli Sattler

Classification

  • Artificial Intelligence / Robotics
  • Verification / Logic

Keywords

  • Propositional satisfiability
  • Description logics
  • Standard and non-standard inferences
  • Reasoning services

Dokumentation

In der Reihe Dagstuhl Reports werden alle Dagstuhl-Seminare und Dagstuhl-Perspektiven-Workshops dokumentiert. Die Organisatoren stellen zusammen mit dem Collector des Seminars einen Bericht zusammen, der die Beiträge der Autoren zusammenfasst und um eine Zusammenfassung ergänzt.

 

Download Übersichtsflyer (PDF).

Publikationen

Es besteht weiterhin die Möglichkeit, eine umfassende Kollektion begutachteter Arbeiten in der Reihe Dagstuhl Follow-Ups zu publizieren.

Dagstuhl's Impact

Bitte informieren Sie uns, wenn eine Veröffentlichung ausgehend von
Ihrem Seminar entsteht. Derartige Veröffentlichungen werden von uns in der Rubrik Dagstuhl's Impact separat aufgelistet  und im Erdgeschoss der Bibliothek präsentiert.