Supported by the Austrian Science Fund (FWF), Project P 28789-N32 (2016-2019)

Generalization is a process of obtaining more general objects from concrete ones. It is a key concept in inductive reasoning. In its simplest form, generalization of two terms *s* and *t* is a term *r* such that *s* and *t* can be obtained from *r* by some variable substitutions. From all such generalizations, the interesting ones are those that can not be made more specific: least general generalizations.

The process of computing least general generalizations is known as anti-unification. It is a procedure dual to unification, which can be seen as a computation of most general common instances of the given terms (most general specifications).

Current research on anti-unification is dominated by practically oriented topics, which is not surprising, because generalization computation, in various forms, is an important ingredient of many applications in reasoning, learning, information extraction, data compression, software development and analysis, etc.

In this project we address challenges to generalization computation posed by new application domains. Some require studying generalization problems in a completely new theory. Some others may be dealt more adequately by improving existing algorithms. It is well-known that in many applications, the standard first-order anti-unification is too weak. We are concerned with the development of generalization algorithms for equational and higher-order theories (also with respect to special similarity relations and for terms in specific forms), their analysis, investigation of efficient special cases, free open source implementation, and applications.

Software developed in this project is incorporated into the library of unification and anti-unification algorithms.

- A. Baumgartner, T. Kutsia. J. Levy, M. Villaret. Term-Graph Anti-Unification. In: H. Kirchner, editor.
*Proceedings of the 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)*. July 9–12, 2018, Oxford, UK. Volume 108 of the Leibniz International Proceedings in Informatics (LIPIcs). Schloss Dagstuhl, 2018, 9:1–9:16.

- D. Cerna, T. Kutsia. Higher-Order Equational Pattern Anti-Unification. In: H. Kirchner, editor.
*Proceedings of the 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)*. July 9–12, 2018, Oxford, UK. Volume 108 of the Leibniz International Proceedings in Informatics (LIPIcs). Schloss Dagstuhl, 2018, 11:1–11:16.

- T. Kutsia, C. Pau. Proximity-Based Generalization. In: M. Ayala-Rincon and Ph. Balbiani, editors.
*Proceedings of the 32nd International Workshop on Unification (UNIF 2018)*. July 7, 2018, Oxford, UK.

- D. Cerna, T. Kutsia. Towards Generalization Methods for Purely Idempotent Equational Theories. In: M. Ayala-Rincon and Ph. Balbiani, editors.
*Proceedings of the 32nd International Workshop on Unification (UNIF 2018)*. July 7, 2018, Oxford, UK.

- N. Amiridze, T. Kutsia. Anti-Unification and Natural Language Processing. In: A. Asudeh, V. de Paiva, and L. Moss, editors.
*Proceedings of the Fifth Workshop on Natural Language and Computer Science (NLCS 2018)*. July 7, 2018, Oxford, UK.

- S. Alves, B. Dundua, M. Florido, T. Kutsia. Pattern-based calculi with finitary matching.
*Logic Journal of the IGPL*. 26(2):203–243.

PDF from the publisher's page, BibTeX. - D. Cerna, M. P Lettmann. Integrating a Global Induction Mechanism into a Sequent Calculus. In: R. A. Schmidt, C. Nalon, editors. Automated Reasoning with Analytic Tableaux and Related Methods - 26th International Conference, TABLEAUX 2017, BrasÃlia, Brazil, September 25-28, 2017, Proceedings. Lecture Notes in Computer Science 10501, Springer, 2017, 278-294.

PDF, BibTeX. - B. Dundua, T. Kutsia, K. Reisenberger-Hagmayr. An overview of PρLog. In: Y. Lierler and W. Taha, editors.
*Proceedings of the 19th International Symposium on Practical Aspects of Declarative Languages, PADL 2017.*Volume 10137 of of Lecture Notes in Computer Science. Springer, 2017. 34–49.

PDF, BibTeX. - B. Dundua, T. Kutsia, K. Reisenberger-Hagmayr. PρLog: Combining Logic Programming with Conditional Transformation Systems (Tool Description). In: M. Carro, A. King, N. Saeedloei, and M. De Vos, editors.
*Technical Communications of the 32nd International Conference on Logic Programming, ICLP 2016.*Vol. 52 of OpenAccess Series in Informatics (OASIcs). Schloss Dagstuhl, 2016, 10.1–10.5.

PDF, BibTeX. - B. Konev, T. Kutsia. Anti-Unification of Concepts in Description Logic EL. In:
*Proceedings of the 15th International Conference on Principles of Knowledge Representation and Reasoning, KR 2016.*April 25–29, 2016, Cape Town, South Africa. The AAAI Press, 2016. 227–236.

PDF, BibTeX.

Research Institute for Symbolic Computation

Johannes Kepler University Linz

Altenbergerstrasse 69

A-4040 Linz, Austria

Phone: +43 (0)732 2468 9982

kutsia@risc.jku.at