Invited Speakers

Jeremy Avigad (jointly with TABLEAUX). 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.

Maria Paola Bonacina. Conflict-Driven Reasoning in Unions of Theories

Many applications of automated reasoning require decision procedures for the satisfiability of a formula in a theory given by the union of a few theories. Reasoning in a union of theories can be approached in more than one way. The equality-sharing method, also known as Nelson-Oppen scheme, combines decision procedures for the component theories. Superposition-based theorem-proving strategies unite the presentations of the theories to reason about their union. CDSAT, which stands for Conflict-Driven SATisfiability, assumes that each theory is equipped with an inference system, called theory module, and coordinates the theory modules to reason in a conflict-driven manner in the union of the theories. A theory module is an abstraction of a decision procedure, made of inference rules that may correspond to axioms of the theory. Conflict-driven means that the system maintains a representation of a candidate partial model of the formula, and performs nontrivial inference only to explain conflicts between the candidate model and the formula, so that the conflict can be solved by updating the partial model. CDSAT provides a framework where the theory modules cooperate to build the candidate model and to explain the conflicts. This talk presents CDSAT placing it in the big picture of multi-theory reasoning and conflict-driven reasoning.
(Joint work with Stéphane Graham-Lengrand and Natarajan Shankar)

Stéphane Graham-Lengrand. Recent and ongoing developments of model-constructing satisfiability

Model-constructing satisfiability (Jovanović et al.) is an instance of conflict-driven reasoning tailored to theories that have a standard model, typically arithmetic theories. Using that standard model to evaluate terms and formulae is a central part of model-constructing satisfiability, and allows the reduction of ground satisfiability problems to (series of) interpolation problems. These problems have a specific form that strongly relates to quantifier elimination. We will illustrate the approach with linear rational arithmetic, and present more recent work on the theory of bitvectors and propositional intuitionistic reasoning. Finally we will discuss the generalisation of model-constructing satisfiability to quantified problems, building on the connection with quantifier elimination and with previous work by Bjørner and Janota on quantified satisfaction.

Uli Sattler (jointly with TABLEAUX). 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.