Invited speakers

Jeremy Avigad (jointly with FroCoS). Automated Reasoning for the Working Mathematician

The mathematical literature is filled with minor errors and imprecision, and interactive proof assistants offer hope for making mathematics more reliable and exact. Given the gap between an informal proof and a formal derivation, one would expect automated reasoning tools to play a key role in formally verified mathematics. But this expectation has not been borne out in practice. Despite technological advances, automated reasoning is far from central to the field, and many the most impressive accomplishments to date have used surprisingly little automation. The use of automated reasoning tools in mathematical discovery has been even more limited. In this talk, I will do my best to make sense of this state of affairs and offer guidance towards developing useful mathematical tools.

Stéphane Graham-Lengrand & Sara Negri (special talk in the honor of Roy Dyckhoff)

Uli Sattler (jointly with FroCoS) Modularity and Automated Reasoning in Description Logics

Description Logics are decidable fragments of first order logics closely related to modal logics and the guarded fragment. Through their use as logical underpinning of the Semantic Web Ontology Language OWL, they are now widely used in a range of areas, DL reasoners have to deal with logical theories — called ontologies — of increasing size and complexity, and domain experts using DLs ask for increasingly sophisticated tool support. One of the many areas that have been considered in this aspect is modularity, a concept that has proven useful to tame complexity and enable separation of concerns in other areas, in particular Software Engineering. In this talk, I will try to give an overview of work in this area.

Firstly, we consider the task of extracting, from one ontology, a small/suitable fragment that captures a given topic (usually described in terms of its signature). The question of suitability versus size here is interesting, and has given rise to different notions of modules and their properties and algorithms for their extraction. Secondly, it would be extremely useful if we could “modularise” a large ontology into suitable coherent fragments (OWL has an “imports” construct that supports some kind of modular working with an ontology). Thirdly, if we have such a nice, modular ontology, how can a group of domain experts work independently on these without undesired side effects. Fourth and finally, reasoning over ontologies is often a highly complex task, and a natural question arising is whether/which form of modularity can be used and how to optimise reasoning.