2nd Semester 2024/25: Automated Equational Reasoning via Rewriting

Instructors

Andrés Goens, Balder ten Cate

ECTS

6

Description

Equational reasoning deals with theories defined by sets of equations that hold of that theory, for example many algebraic structures, but also lambda calculi or programming languages. There are many established techniques that let us reason about these equational theories automatically. These are at the heart of many modern automated reasoning systems, like modern SMT solvers or many resolution-based provers. In this course we will learn some of the main techniques, like term rewriting, Knuth-Bendix complition or E-graphs and equality saturation, as well as examples of equational theories.

Organisation

After two introductory lectures (Week 1), students will choose topics to deepen into (Week 2). These might be some of the techniques we outlined, or specific equational theories to investigate further. They will work on a self-organized project (Week 3), e.g. implementing the algorithm they investigated, or proving properties about the equational theory they chose, or something in-between. At the end of the block (Week 4) we will have a round of presentations where these short projects will be presented.

Prerequisites

Mostly "mathematical maturity", you should have seen a few logics or formal languages, but that should be the case for every MoL student.

Assessment

 Presentation at the end of the month.

References

 Baader, Franz, and Tobias Nipkow. Term rewriting and all that. Cambridge university press, 1998.