Sistemas de Reescrita

Objectivos

Domínio dos conceitos fundamentais dos sistemas de reescrita, tais como os de terminação e confluência.

Saber provar os resultados básicos da teoria de sistemas de reescrita, entre os quais o teorema dos pares críticos.

Saber aplicar os resultados fundamentais da teoria em apresentações de semigrupos e bases de Grobner.

Reconhecer a aplicação destes conceitos em alguns sistemas computacionais, como por exemplo na computação algébrica simbólica, na prova automática de teoremas, na especificação e verificação de programas e na programação de linguagens de ordens superiores.

Caracterização geral

Código

8417

Créditos

6.0

Professor responsável

A disponibilizar brevemente

Horas

Semanais - 4

Totais - 16

Idioma de ensino

Português

Pré-requisitos

A disponibilizar brevemente

Bibliografia

• F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.

• B. Benninghofen, S. Kemmerich and M. M. Richter. Systems of Reductions. Lecture Notes in Computer Science, vol. 277. Springer-Verlag, 1987.

• R.V. Book and F. Otto. String-Rewriting Systems. Springer-Verlag, 1993.

• TERESE, Term Rewriting Systems, Cambridge University Press, 2003.

• E. Ohlebusch. Advanced Topics in Term Rewriting. Springer-Verlag, 2002.

Método de ensino

A disponibilizar brevemente

Método de avaliação

A disponibilizar brevemente

Conteúdo

1. Sistemas abstractos de redução: reduções e equivalências; indução transfinita; relações de ordem.

2. Sistemas de reescrita de termos: termos, substituições e identidades; álgebras livres; álgebras de termos; classes equacionais; problemas equacionais.

3. Sistemas de reescrita de palavras: congruências de Church-Rosser; o problema da palavra; semigrupos e apresentações.

4. Terminação: o problema de decisão; ordens de redução; ordens de simplificação.

5. Confluência: confluência e confluência local; o problema de decisão; pares críticos.

6. Completude: o procedimento de Knuth-Bendix.

7. Bases de Grobner: redução de polinómios; bases de Grobner; algoritmo de Buchberger.

Cursos

Cursos onde a unidade curricular é leccionada: