Re: [Logica-l] ATPs (Automatic Theorem Provers) para Lógicas Não-Clássicas

2017-05-30 Por tôpico Joao Marcos
> 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. Achei hoje por acaso o link para muita diversão intuicionista ou mi

Re: [Logica-l] ATPs (Automatic Theorem Provers) para Lógicas Não-Clássicas

2017-04-26 Por tôpico Marcelo Finger
Olá JM. Imagino que a diminuição de 1936 casos para "só" 633 configurações seja um exercício intelectual nada trivial. Geradores automáticos têm a tendência (não a promessa) de ir no sentido oposto, usar a força bruta e velocidade da máquina, passar de 633 para 6.330 se isso garantir que testar "

Re: [Logica-l] ATPs (Automatic Theorem Provers) para Lógicas Não-Clássicas

2017-04-25 Por tôpico Joao Marcos
2017-04-26 2:55 GMT+02:00 Marcelo Finger : > > Sobre provas geradas automaticamente, em especial para o caso da > 4-coloração, avento a possibilidade de que uma prova automaticamente > gerada (e verificada) possa term MAIS CASOS que a atualmente > conhecida. > > Aliás, isso seria o esperado. Se é

Re: [Logica-l] ATPs (Automatic Theorem Provers) para Lógicas Não-Clássicas

2017-04-25 Por tôpico Walter Carnielli
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

Re: [Logica-l] ATPs (Automatic Theorem Provers) para Lógicas Não-Clássicas

2017-04-25 Por tôpico Renata Wassermann
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.c

Re: [Logica-l] ATPs (Automatic Theorem Provers) para Lógicas Não-Clássicas

2017-04-25 Por tôpico Joao Marcos
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

Re: [Logica-l] ATPs (Automatic Theorem Provers) para Lógicas Não-Clássicas

2017-04-24 Por tôpico Valeria de Paiva
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 P

Re: [Logica-l] ATPs (Automatic Theorem Provers) para Lógicas Não-Clássicas

2017-04-24 Por tôpico Cláudia Nalon
Caro Walter, Existem vários provadores automáticos para lógicas não-clássicas. Para lógicas modais, por exemplo, um bom ponto de partida é lista mantida pela Renate Schmidt: http://www.cs.man.ac.uk/~schmidt/tools/ Abraços, Cláudia Em 2017-04-24 22:03, Walter Carnielli escreveu: Caros Coleg

[Logica-l] ATPs (Automatic Theorem Provers) para Lógicas Não-Clássicas

2017-04-24 Por tôpico Walter Carnielli
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, axiomati