Algebra Seminar talk
2026-03-13
Johannes Weiser
Definability of Sets of Arrays
Abstract:
Definability is one of the most central concepts in model
theory. In this talk, we consider the theory of arrays, a first-order
theory that is used for software verification. Knowing which sets can
be defined by certain formulas yields interesting results concerning
software verification. In this talk, we present undefinability results
for quantifier-free formulas, $\Sigma_1$-formulas and the universal
array property fragment in the theory of arrays. Furthermore, we
present open questions in this context that arise when trying to push
this research further.