Oi Valéria, Não tem problema :)
>acho que seria legal se a gente unisse os esforcos pra fazer todos os >lambda-termos pros teoremas intuicionistas do Kleene em (S. C. Kleene. >Introduction to metamathematics, volume 1 of Bibliotheca mathematica. >NorthHolland Publishing Co., 1952.). Essa me parece uma ótima ideia! Atualmente o Cubo prova todos os teoremas da lógica proposicional intuicionística (e clássica, via e.g. a inclusão da lei do terceiro excluído no contexto de premissas) e também realiza quaisquer operações aritméticas e booleanas que não envolvem tipos dependentes. Para provar o resto dos teoremas do Kleene, no entanto, precisariamos de dependência de tipos e tipos de identidade - o que é bom, pois esse é o objetivo a longo prazo. Tenho algumas ideias de como estender o sistema, mas no momento me falta tempo livre para sentar e me preparar para a inevitável dor de cabeça :) Abraços lógicos, Bruno -- Bruno Bentzen https://sites.google.com/site/bbentzena/ -- Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" dos Grupos do Google. Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para logica-l+unsubscr...@dimap.ufrn.br. Para postar neste grupo, envie um e-mail para logica-l@dimap.ufrn.br. Visite este grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/. Para ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/d021bed4-6cde-4494-a331-b79a95e04678%40dimap.ufrn.br.
