oi Walter, existem alguns, mas nao sao tao bacanas quanto a gente gostaria!...
mesmo pra logica intuicionista a coisa nao esta' tao desenvolvida. Da mesma forma que pra logica classica (proposicional e de primeira ordem) existe a TPTP Library- http://www.cs.miami.edu/~tptp/ (TPTP --Thousands of Problems for Theorem Provers-- a library of test problems for automated theorem proving <http://www.cs.miami.edu/%7Etptp/OverviewOfATP.html> (ATP) systems. ) tem uma testsuite pra logica intuicionista do Jens Otten and Thomas Raths em http://www.iltp.de/index.html. mas tem bem menos provadores e eles nao estao tao desenvolvidos. PRa logica modal tem duas dessas libraries de problemas: http://www.iltp.de/qmltp/ (Otten again) e a do Chris Benzmueller. PRa Logica Linear eu e a Giselle Reis comecamos a tentar organizar uma colecao de problemas tambem, mas estamos so' comecando a tentar comparar os provadores que conhecemos. Mas e', os teoremas mais interessantes sao os provados por sistemas interativos, guiados pelos humanos, onde o computador faz a parte chata e bracal e os humanos entram com as ideias. George Gonthier, um amigo de muitos anos, e' uma das figuras famosas, liderando o time que provou de novo o teorema das 4 Cores e mais recentemente o Feit-Thompson theorem, part of the classification of finite simple groups <https://en.wikipedia.org/wiki/Classification_of_finite_simple_groups>. (a classificacao dos grupos simples e' um tour de force da matematica relativamente recente, mas o que e' surpreendente no uso de provadores nao sao os teoremas, 'e a dificuldade de se entender as provas produzidas. o Leonardo de Moura (que foi da PUC e agora e' Microsoft Research) tb lidera com seu provador de hardware e mais recentemente com Lean, que ele e Jeremy Avigad estao querendo usar pra fundamentos da matematica. veja https://leanprover.github.io/people/. e' uma area fascinante, mas complicada, pois os provadores tendem a ficar bem complicados bem rapidamente... abs Valeria 2017-04-24 18:03 GMT-07:00 Walter Carnielli <[email protected]>: > Caros Colegas que usualmente falam sobre ATPs (Automatic Theorem > Provers): > (Elaine, João Marcos, Valéria, Marcelo Finger entre outros) > > 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'. > > Abraços, > Walter > > > -- > ----------------------------------------------- > Walter Carnielli > Centre for Logic, Epistemology and the History of Science and > Department of Philosophy > State University of Campinas –UNICAMP > 13083-859 Campinas -SP, Brazil > Phone: (+55) (19) 3521-6517 > Institutional e-mail: [email protected] > Website: http://www.cle.unicamp.br/prof/carnielli > > -- > 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/di > map.ufrn.br/group/logica-l/. > Para ver esta discussão na web, acesse https://groups.google.com/a/di > map.ufrn.br/d/msgid/logica-l/CA%2Bob58PkkSA0yZymLN0k0qhuP8O > oUs-J3NHF63Y_essLAXbmyg%40mail.gmail.com. > -- Valeria de Paiva http://vcvpaiva.github.io/ http://research.nuance.com/author/valeria-de-paiva/ http://www.cs.bham.ac.uk/~vdp/ -- 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/CAESt%3DXu-ZE4y5b6BvpmeBDie5oJx9qSgaBw2keP0c5LSNCcOUg%40mail.gmail.com.
