Sistemas de Reescrita
Objetivos
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.