MAT Palestras - Teoria da Computação

Anti-unification modulo syntactic, associative and commutative equational theories

Nesta palestra apresentaremos o módulo do problema da anti-unificação as teorias equacionais vazias, associativas e comutativas. Mostraremos as regras de simplificação de cada um desses casos e as discutiremos por meio de exemplos, apontando os diferentes resultados obtidos para cada teoria equacional. O objetivo é analisar as propriedades de terminação, confluência e correção dos algoritmos anti-unificação.
Gabriela de Souza Ferreira PPGMAT- UnB em 22/10/2021

Abstract

The anti-unification problem is concerned about finding the least general generalization of a couple of terms, say s and t. In other words, it is the problem of finding a term r that could “represent” either both terms via substitutitions σ1 and σ2, that is, σ1r = s and σ2r = t.
In this talk we will present the anti-unification problem modulo the empty, associative and commutative equational theories. We will show the simplification rules of each of these cases and discuss them by examples, pointing out the different results obtained for each equational theory. The purpose is analyse the termination, confluence and correctness properties of the anti-unification algorithms.

Local e Data

Tema: Anti-unification modulo syntactic, associative and commutative equational theories
Palestrante: Gabriela de Souza Ferreira PPGMAT- UnB
Data: 22/10/2021