Extensional theories and rewriting

Abstract

This paper is an attempt to develop a unifying algebraic framework for extensional theories capturing formally the informal concept of extensionality, as well as a generic automated proving technique, called extensional rewriting, that can be instantiated and then used to prove equational properties in various particular extensional theories. © Springer-Verlag Berlin Heidelberg 2004.