Walter, e demais colegas: > Existem ATPs bacanas para Lógicas Não-Clássicas? Para a Logica > Intuicionista certamente existem, e sei (por trabalhar com tablôs, > dedução natural, axiomaticas hilbertianas, etc) que certamente se > podem adaptar Isabelle, Mizar, etc, para isso. Mas eu gostaria de > saber se há ATPs que são 'nativos' de Lógicas Não-Clássicas,e o que > eles já demonstraram (se é que...) de 'surpreendente'.
A lista que a Cláudia mandou é ótima, e o material do Otten que a Valeria apontou também! Com relação a demonstradores computacionais _assistidos por humanos_, o meu atual favorito é de fato o Lean, desenvolvido pelo Leonardo de Moura. Como provavelmente seria de se esperar, os demonstradores _automáticos_ não são em geral construídos para *lógicas* específicas, mas para *sistemas dedutivos* específicos. Os dois sistemas online que eu usei mais recentemente foram: MetTel 2 (http://www.mettel-prover.org/demo.php) Gen2Sat (http://gen2sat-yonizohar.rhcloud.com/gen2sat/?id=blank) O MetTel é um demonstrador genérico baseado em *tableaux*, no qual é bastante fácil definir a sintaxe e as regras da lógica em questão, e gerar a partir daí um demonstrador "nativo" para esta lógica. O Gen2Sat é ainda mais simples de se usar, embora um pouco menos "customizável", e se baseia em *cálculos de sequente* analíticos, cujos procedimentos de decisão são traduzidos e enviados para serem tratados por solucionadores SAT genéricos. Com relação a demonstrações surpreendentes, acho que isto dependo do que você entende por "surpreendente"! Com relação à lógica intuicionista, em particular, a família Loparic tinha implementado online um demonstrador baseado na semântica de valorações da Andrea. Neste momento não estou achando, contudo, o link para o sistema. Elaine e Giselle também colocaram online alguns demonstradores para lógicas lineares e modais. A Cláudia tem implementado vários sistemas para lógicas não-clássicas baseados em resolução. Certamente elas poderão lhe esclarecer melhor, em primeira mão, sobre seus trabalhos! Finalizo acrescentando apenas uma pequena clarificação. A Valéria escreveu: > > George Gonthier, um amigo de muitos anos, e' uma das figuras > famosas, liderando o time que provou de novo o teorema das 4 Cores Vale notar, contudo, que o que o Gonthier (Microsoft Research Cambridge) produziu em 2005 não foi apenas uma nova demonstração do teorema das quatro cores na qual o computador é usado na sub-tarefa de checagem exaustiva de um grande número de reduções dos mapas, como fizeram Appel & Haken na década de 70, mas sim uma demonstração *inteiramente* produzida com o auxílio de um demonstrador automático (no caso, o Coq). Isto consiste no que o Gonthier chama de "formal program proof", a saber, código que diz não apenas *o quê* a máquina deve fazer, mas também o *por quê* (entendendo por isto que o código deve conter uma "computer-checked proof of correctness"). Abraços, Joao Marcos -- http://sequiturquodlibet.googlepages.com/ -- 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 [email protected]. Para postar neste grupo, envie um e-mail para [email protected]. 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/CAO6j_Lhc7EFrv86FSYMa2sfYLv3YJ-ERU3V0nu4we_TYGnmgjA%40mail.gmail.com.
