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.