Further development and use of the unification and generalization algorithm library

Further development and use of the unification and generalization algorithm library (Advisor: Teimuraz Kutsia). At RISC, we have been developing an open source library of unification and generalization algorithms, currently hosted at https://www1.risc.jku.at/projects/stout/ Unification is a process of equation solving, aiming at computing a most general common instance of the terms involved. Anti-unification is its dual process, aiming at computing a least general common generalization of the input terms (retaining their common structure as much as possible). The topics are for one or more bachelor theses: Extend the library by implementing recently developed improvements of some of the algorithms already in the library; add a new algorithm for term-graph generalization; add an algorithm for context sequence matching with regular constraints; experimental applications. Prerequisites: Programming in Java (since the library is written in Java), basic knowledge of logic, some familiarity with declarative programming and automated reasoning is a plus.

At RISC, we have been developing an open source library of unification and generalization algorithms, currently hosted at
https://www1.risc.jku.at/projects/stout/

Unification is a process of equation solving, aiming at computing a most general common instance of the terms involved. Anti-unification is its dual process, aiming at computing a least general common generalization of the input terms (retaining their common structure as much as possible).

The topics are for one or more bachelor theses: Extend the library by
implementing recently developed improvements of some of the algorithms already in the library; add a new algorithm for term-graph generalization; add an algorithm for context sequence matching with regular constraints; experimental applications.

Prerequisites: Programming in Java (since the library is written in Java), basic knowledge of logic, some familiarity with declarative programming and automated reasoning is a plus.