Brigitte Pientka: Eliminating Redundancy in Higher-Order Unification: A Lightweight Approach. IJCAR 2006: 362-376