Car@s, Muitíssimo obrigado à Cláudia, Valéria, Renata e João Marcos pelos excelentes `reports'. Teria levado meses para chegar a isso, se chegasse!
Aproveito meus agradecimentos para contar, no interesse da Lógica, porque isso me interessa. Xavier Caicedo provou em ''The subdirect decomposition theorem for classes of structures closed under direct limits'' (J. Austral. Math. Soc. Series 4, 30 (1980), 171-179) uma generalização de um teorema de Birkhoff, mostrando que toda álgebra (numa classe K de álgebras definidas por meio de equações) é um produto subdireto de álgebras subdiretamente irredutíveis em K. Há anos e anos atrás, em conversas (nem sei se isso está publicado) Caicedo me convenceu de que se pudéssemos provar uma versao construtiva desse fato, isso geraria uma prova sintética do Teorema das Quatro Cores. Na Dissertação de Mestrado do Pedro Catuogno de mais de 20 anos (IMECC) tentamos formalizar isso, e encontrar essa prova ''na unha'', mas não conseguimos (caso contrário, vocês nos teriam visto na primeira página do New York TImes) embora algumas coisinhas menores tivessem saido. Agora, com esse avanço desconhecido na época, como tenho um ótimo estudante de Graduação interessadísimo no tema, vamos apoveitar o embalo... Não creio que consigamos - mas como me disse o Dória há anos atrás (talvez ele se lembre) a vida é curta demais para que nos interessemos pelos problemas fáceis :-) Qualquer ajuda, **parceria**, comentário, puxão de orelha, etc, é ultra-benvinda(o). Por enquanto só sei arranhar a superfície dos provadores automáticos... Abraços, Walter Em 25 de abril de 2017 08:59, Renata Wassermann <[email protected]> escreveu: > Para aumentar um pouco a lista: > > - Existem montes de provadores para lógicas de descrição de expressividades > variadas. Alguns estão na lista que a Valéria postou, mas os mais usados - > HermiT e Pellet - não estão lá. Uma lista especifica para DLs e ontologias > pode ser encontrada em > http://owl.cs.manchester.ac.uk/tools/list-of-reasoners/ > > - Existem também provadores para lógicas não-monotônicas. O caso de maior > sucesso em termos de implementação é ASP (Answer Set Programming), por > exemplo o Potassco (https://potassco.org/). > > Abraços, > > Renata. > > On Tuesday, April 25, 2017 at 4:11:00 AM UTC-3, Joao Marcos wrote: >> >> 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"). >> -- 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/CA%2Bob58ObugutKxmypVQ43dCPwZd0h34uDDSXJsQy_QCMMS3FKQ%40mail.gmail.com.
