Algorithms for Equality and Unification in the Presence of Notational Definitions
Frank Pfenning, Carsten Schürmann · Electronic Notes in Theoretical Computer Science · 1998
Notational definitions are pervasive in mathematical practic and are therefore supported in must automated theorem proving systems. In this paper we investigate their interaction with algorithms for testing equality and unification. We propose a syntactic criterion on definitions which avoids their expansion in many cases without losing soundess or completeness with respect to βηδ-conversion.