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"). > > 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/b96a3b25-6fd0-4428-8a26-d9581c2a56fe%40dimap.ufrn.br.
