Modeling reducibility on ground terms using constraints
Isabelle Gnaedig, Claude Kirchner · HAL (Le Centre pour la Communication Scientifique Directe) · 2009
In this note, we explain how to model (ir)reducibility of rewriting on ground terms using (dis)equational constraints. We show in particular that innermost (ir)reducibility can be modeled with a particular narrowing relation and that (dis)equational constraints are issued from the most general unifiers of this narrowing relation.