MAT Palestras - Teoria da Computação

Lifting the Nominal Commutative Narrowing

Nosso objetivo nesta palestra é estender um dos resultados mais importantes do estreitamento – o Teorema do Elevação – para o arcabouço nominal considerando o caso comutativo. Em particular, discutiremos as dificuldades para obter provas de exatidão e completude neste cenário de comutatividade módulo estreitamento nominal.
Daniella Santaguida - UnB em 25/03/2022

Abstract

Narrowing is a well-known approach for equational unification, that is, to solve term equations modulo an equational theory E. It is complete whenever the equational theory E is presented as a convergent rewrite system. Our goal in this talk is to extend one of the most important results of related to narrowing – the Lifting Theorem - to the nominal framework considering the commutative case. In particular, we will discuss the difficulties to obtain correctness and completeness proofs in this setting of nominal narrowing modulo commutativity.

Local e Data

Tema: Lifting the Nominal Commutative Narrowing
Palestrante: Daniella Santaguida - UnB
Data: 25/03/2022