RISC JKU
  • @techreport{RISC5918,
    author = {David M. Cerna and Temur Kutsia},
    title = {{Higher-Order Pattern Generalization Modulo Equational Theories}},
    language = {english},
    abstract = {In this paper we address Three problems related to unital anti-unification. First, we develop a general algorithm based on a tree grammar representation of the set of computed generalizations. Secondly we show that restricting the algorithm to computing linear generalizations only or to term signatures containing a single unital function results in a procedure which is minimal complete and Finitary. Thirdly, we show that when the term signature contains two unital functions, unital anti-unification is Nullary. The algorithm does not depend on the number of idempotent function symbols in the input terms. The language generated by the grammar is the minimal complete set of generalizations of the given anti-unification problem, which implies that idempotent anti-unification is infinitary.},
    year = {2019},
    length = {40},
    type = {RISC Report Series},
    institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
    address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
    }