Automated Reasoning -- Core Algorithms and Data Structures

                   Stephan Schulz

We will look at some core concepts shared by nearly all modern
automated theorem provers and related systems -- terms, substitutions,
unification, matching, as well as their applications, including
paramodulation/superposition, rewriting, and subsumption. I will
present actual code examples from PyRes and E, and discuss some
implementation details.

We will then also attempt to develop a new, unification-based clause
selection heuristic for E, and evaluate if it is a useful contribution
to the portfolio of strategies.

Participants are encouraged to bring a laptop with a UNIX/Linux style
C development system, and/or a recent Python-3 installation for the
practical work.