Synthesis of rewrite programs by higher-order and semantic unification
scientific article; zbMATH DE number 4172397