Abstract:
Generalization of two or more objects (terms, trees, forests, graphs, formulas, proofs, programs, …) is an object, which keeps common features of the given objects and shows how they differ. It is a fundamental concept for tasks where one is interested in extracting a common general pattern from the given concrete examples.
Anti-unification is a logic-based method to compute generalizations. It was introduced in the 1970s, motivated by an application in inductive reasoning. In recent years, there has been growing interest in anti-unification due to novel applications in various subareas of artificial intelligence and computer science, where anti-unification-based techniques have been successfully applied in analogical reasoning, logic-based learning, term set compression, program synthesis, programming by examples, software code clone detection, automated program repair, library learning, etc.
In this talk, we will give a survey on recently developed generalization algorithms in first-order and higher-order theories, consider their applications, and discuss some interesting research problems in this area.
Short Bio:
Temur Kutsia is a senior researcher and associate professor at the Research Institute for Symbolic Computation (RISC) Institute of the Johannes Kepler University Linz, Austria, where he leads a research group on symbolic constraint solving. He obtained his PhD and habilitation from Johannes Kepler University. His research interests lie in computational logic and symbolic artificial intelligence, with a particular focus on equational constraint solving, unification and generalization, as well as rewriting-based deduction and computation. He has authored over 100 publications in these areas, edited 20 conference proceedings and journal special issues, and served on more than 100 program committees of international conferences. He is a member of the IFIP Working Group 1.6 (Term Rewriting) and serves on the editorial board of the Journal of Symbolic Computation.
