O CEMS.UL convida para a participação na palestra sobre conversões comutativas são frequentemente consideradas artificiais ou conceitualmente insatisfatórias, levantando questões sobre a adequação dos formalismos sintáticos. Nesta palestra, revisita-se essa questão apresentando traduções do Cálculo Proposicional Intuicionista (IPC) para sistemas de prova onde as conversões comutativas não ocorrem.
Um exemplo bem conhecido de tais traduções é a incorporação de IPC no Sistema F por Russell-Prawitz, que, apesar de sua elegância, não preserva a redução de provas nem a identidade de provas.
Apresentam-se duas estratégias para lidar com esse problema. Uma refina o sistema de destino, restringindo o polimorfismo de forma atómica. A outra introduz conversões adicionais no sistema de destino para lidar com a atomização. Ambas as estratégias preservam a identidade da prova, mas até recentemente, apenas a segunda estratégia era conhecida por garantir a preservação da redução da prova. Uma tradução recente mostra que também é possível, através da primeira estratégia, preservar a redução, evitando completamente as conversões comutativas. Nesta abordagem, as conversões comutativas colapsam para a identidade sintática, fornecendo uma imagem do IPC livre de conversões comutativas.
Apresentação por Gilda Ferreira (Universidade Aberta, CEMS.UL)
Esta apresentação inclui um trabalho conjunto significativo com José Espírito Santo.
Data de realização: 20 janeiro 2026 às 15h00 na sala 6.2.33 na Ciências ULisboa