Eine Methode zur automatischen Herleitung oder Widerlegung einfacher Programmeigenschaften durch Generierung neuer Termersetzungsregeln. - Martin Müller 006 (1999)