ATPs (Automatic Theorem Provers) para Lógicas Não-Clássicas
44 views
Skip to first unread message
Walter Carnielli
Apr 24, 2017, 9:03:48 PM4/24/17
to Lista dos Logicos Brasileiros
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: walter.c...@cle.unicamp.br
Website: http://www.cle.unicamp.br/prof/carnielli
(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: walter.c...@cle.unicamp.br
Website: http://www.cle.unicamp.br/prof/carnielli
Cláudia Nalon
Apr 24, 2017, 10:00:00 PM4/24/17
to logi...@dimap.ufrn.br
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
--
Cláudia Nalon
------------------------------------
Departmento de Ciência da Computação
Instituto de Ciências Exatas
Universidade de Brasília
http://www.cic.unb.br/~nalon
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
Cláudia Nalon
------------------------------------
Departmento de Ciência da Computação
Instituto de Ciências Exatas
Universidade de Brasília
http://www.cic.unb.br/~nalon
Valeria de Paiva
Apr 25, 2017, 12:26:33 AM4/25/17
to Lista acadêmica brasileira dos profissionais e estudantes da área de LOGICA
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 (ATP) systems. )
tem uma testsuite pra logica intuicionista do Jens Otten and Thomas Raths
em http://www.iltp.de/index.html. 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 (ATP) systems. )
mas tem bem menos provadores e eles nao estao tao desenvolvidos.
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...
Valeria
--
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 logica-l+u...@dimap.ufrn.br.
Para postar neste grupo, envie um e-mail para logi...@dimap.ufrn.br.
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%2Bob58PkkSA0yZymLN0k0qhuP8OoUs-J3NHF63Y_essLAXbmyg%40mail.gmail.com.
--
Joao Marcos
Apr 25, 2017, 3:11:00 AM4/25/17
to Lista acadêmica brasileira dos profissionais e estudantes da área de LOGICA
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:
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/
> 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'.
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
> George Gonthier, um amigo de muitos anos, e' uma das figuras
> famosas, liderando o time que provou de novo o teorema das 4 Cores
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/
Renata Wassermann
Apr 25, 2017, 8:23:36 AM4/25/17
to LOGICA-L
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.
- 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.
Walter Carnielli
Apr 25, 2017, 10:37:35 AM4/25/17
to Lista dos Logicos Brasileiros
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
<renat...@gmail.com> escreveu:
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
<renat...@gmail.com> escreveu:
Joao Marcos
Apr 26, 2017, 2:49:59 AM4/26/17
to Lista acadêmica brasileira dos profissionais e estudantes da área de LOGICA
2017-04-26 2:55 GMT+02:00 Marcelo Finger <mfi...@ime.usp.br>:
>
> 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 é fácil gerar e verificar casos, é
> provável que seja assim programado.
Confesso que não sei dizer se a demonstração automatizada tem mais
casos do que os que seriam previstos... Na demonstração original de
Appel & Haken [1976] havia 1936 mapas "minimais" com 5 cores a
analisar (a estratégia da demonstração, seguindo a ideia principal da
demonstração errada publicada por Kempe em 1879, é justamente a do
raciocínio por absurdo, mostrando que cada uma destas configurações
pode ser reduzida a uma configuração menor que ainda necessitaria 5
cores). Em 1996, Robertson et al mostraram que é possível diminuir o
número de casos a considerar para "apenas" 633 configurações. Até
onde sei, foi esta última versão da demonstração que foi formalizada
pelo Gonthier.
Abraços,
Joao Marcos
>
> 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 é fácil gerar e verificar casos, é
> provável que seja assim programado.
Confesso que não sei dizer se a demonstração automatizada tem mais
casos do que os que seriam previstos... Na demonstração original de
Appel & Haken [1976] havia 1936 mapas "minimais" com 5 cores a
analisar (a estratégia da demonstração, seguindo a ideia principal da
demonstração errada publicada por Kempe em 1879, é justamente a do
raciocínio por absurdo, mostrando que cada uma destas configurações
pode ser reduzida a uma configuração menor que ainda necessitaria 5
cores). Em 1996, Robertson et al mostraram que é possível diminuir o
número de casos a considerar para "apenas" 633 configurações. Até
onde sei, foi esta última versão da demonstração que foi formalizada
pelo Gonthier.
Abraços,
Joao Marcos
Marcelo Finger
Apr 26, 2017, 7:43:53 AM4/26/17
to logi...@dimap.ufrn.br
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 "só" esses 6 mil e tantos
casos resolvem o problema.
[]s
--
Marcelo Finger
Departament of Computer Science, IME
University of Sao Paulo
http://www.ime.usp.br/~mfinger
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 "só" esses 6 mil e tantos
casos resolvem o problema.
[]s
> --
> 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 logica-l+u...@dimap.ufrn.br.
> Para postar neste grupo, envie um e-mail para logi...@dimap.ufrn.br.
> 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/CAO6j_LgphyNLZSRJyrfmMzga7UtRebWyyc7gZL6m%2BHWPpdTruQ%40mail.gmail.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 logica-l+u...@dimap.ufrn.br.
> Para postar neste grupo, envie um e-mail para logi...@dimap.ufrn.br.
> Visite este grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.
--
Marcelo Finger
Departament of Computer Science, IME
University of Sao Paulo
http://www.ime.usp.br/~mfinger
Joao Marcos
May 30, 2017, 5:09:25 AM5/30/17
to Lista acadêmica brasileira dos profissionais e estudantes da área de LOGICA
> 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
> 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.
minimal-intuicionista:
http://www.paralogics.net/tableaux/minimal_intuitionism/
Consta que o algoritmo foi implementado em Python, e o melhor é que
ele segue funcionando na web desde 2009!
JM
--
http://sequiturquodlibet.googlepages.com/
Reply all
Reply to author
Forward
0 new messages