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