Contact: Teimuraz Kutsia
Short Description: At RISC, we have been developing an open source library of unification and generalization algorithms, currently hosted at http://www.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.