> 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
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 "
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 é
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
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
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
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
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
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