Prezados colegas, Gostaria de apresentar o sistema TATU, desenvolvido por Vivek Nigam e Giselle Reis, que é um: "Online system for reasoning about sequent calculus specifications in linear logic with subexponentials". O sistema ainda está na versão beta, disponível online no endereço:
http://www.logic.at/people/giselle/tatu/ É um sistema muito bonitinho que permite, em particular, checar se um determinado sistema analitico (à la Gentzen e especificado em SELLF) possui a propriedade de cut-elimination. A prova se dá em duas etapas, primeiro verificando se todas as ocorrências da regra cut podem ser transformadas para "principais" e depois se cuts principais podem ser transformados em cuts atômicos. Ainda falta a parte de eliminação de cuts atômicos, mas essa é a parte mais fácil. Saludos, -- Elaine. -------------------------------------------------------- Elaine Pimentel Departamento de Matematicas Universidad del Valle Calle 13 No. 100 - 00 ; Edificio 320. Ciudadela Universitaria Melendez Cali, Colombia https://sites.google.com/site/elainepimentel/ -------------------------------------------------------- _______________________________________________ Logica-l mailing list [email protected] http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
