Automated Reasoning: Between Mathematics and Computer Science

In this talk we give an overview of automated reasoning methods, emphasizing the strong links be-
tween mathematics and computer science.

We start by presenting general automated reasoning methods in algebra and logic having in common
the idea of "completion", namely the computation of Gröbner bases in polynomial ideals, the critical
pair/completion algorithm for equational theories, the resolution principle and one of its refinements
that allows for efficient handling of equality.
We discuss the ways these methods can be used for automated reasoning in mathematics, as well as
their limitations.

One of the limitations is given by the undecidability of first-order logic. Another limitation is the fact
that many problems in mathematics and computer science are heterogeneous in nature:
In mathematical analysis, for instance, we need to reason about functions f: Rn → R satisfying addi-
tional conditions.
While decision procedures for the reals (or for real closed fields) exist -- the theory is known to have
quantifier elimination -- such specialized decision procedures cannot usually handle additional func-
tion symbols.

In order to address these aspects, in the second part of the talk we discuss possibilities of recognizing
problems which are decidable, possibly with low complexity, and possibilities of efficient reasoning in
extensions of a "base" theory with new function symbols satisfying a set of additional axioms. We show
how ideas independently studied in computer science and mathematics come together and can be
extended in order to yield possibilities of recognizing decidable and tractable problems in mathemat-
ics, but also in verification.

We end with some general remarks on automated reasoning, and explain some of the challenges faced
when attempting to solve open problems using computers.

Wann 17.01.2019
von 16:30 bis 18:00
Wo G 209
Teilnehmer Prof. Dr. Viorica Sofronie-Stokkermans, Universität Koblenz-Landau, FB 4: Informatik
Termin übernehmen vCal
abgelegt unter: ,