Room P3.10, Mathematics Building

Luís Cruz-Filipe, U Nijmegen, Netherlands

Hierarchical reflection

Reflection-based tactics are very useful in theorem proving. When doing reflection one defines a type of syntactic expressions that get interpreted in the domain of discourse. By allowing the interpretation function to be partial, one gets a more general method known as partial reflection. In this talk we show how partial reflection can be used to define a tactic for proving equalities in a field in such a way that it will also work in simpler algebraic structures, such as groups and rings.