Ontologia SUMO, ATP, ITP e Explicação de provas
30 views
Skip to first unread message
Alexandre Rademaker
Jun 13, 2016, 12:31:56 PM6/13/16
to Lista acadêmica brasileira dos profissionais e estudantes da área de LOGICA
Prezados,
Estamos fazendo vários experimentos com a SUMO [1], sua tradução para TPTP/FOL [2] e verificação automática em provadores como E, Vampire etc. Estamos reportando várias inconsistencias [3] e dificuldades de obter provas que deveriam ser simples como o exemplo de Banana Slug [4].
Em especial, estou procurando agora boas ferramentas interativas que aceitei como entrada TPTP, debugar provas longas de refutação não é tarefa fácil... Dicas? Alguém conhece algo pronto?!
Ab.,
Hermógenes Oliveira
Jun 14, 2016, 4:20:46 AM6/14/16
to logi...@dimap.ufrn.br
Alexandre Rademaker <arade...@gmail.com> escreve:
> Prezados,
Olá, Alexandre.
> Estamos fazendo vários experimentos com a SUMO [1], sua tradução para
> TPTP/FOL [2] e verificação automática em provadores como E, Vampire
> etc. Estamos reportando várias inconsistencias [3] e dificuldades de
> obter provas que deveriam ser simples como o exemplo de Banana Slug
> [4].
>
> Em especial, estou procurando agora boas ferramentas interativas que
> aceitei como entrada TPTP, debugar provas longas de refutação não é
> tarefa fácil... Dicas? Alguém conhece algo pronto?!
Eu não conheço absolutamente nada sobre ontologia (informática), mas
tenho alguma experiência com o formato TPTP/ILTP.
Se entendi bem o que você precisa, tenho algumas informações que possam
ser relevantes.
Primeiro, baseado numa rápida passada de olhos, me parece que para
resolver o Banana Slug não basta lógica de primeira ordem (TPTP-FOF),
mas é necessário lógica de ordem superior (TPTP-THF)[1].
Quanto a assistentes interativos que trabalhem com o formato TPTP, sei
que o Isabelle contém uma ferramenta tptp_isabelle e que o Matita também
seria capaz de trabalhar com TPTP.
Porém, embora já tenha usado tanto Isabelle quanto Matita, nunca
trabalhei neles com problemas no formato TPTP. Portanto, não sei dizer
se o suporte para TPTP está limitado a FOF ou inclui a extensão para
ordem superior THF.
Dê uma olhada no SystemonTPTP do Prof. Sutcliffe[2]. Talvez encontre
ali no meio um ATP/ITP que satisfaça suas demandas.
Saudações,
Notas:
[1] Imagino que funções indutivamente definidas são necessárias para a
parte aritmética, não?
[2] http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTP
--
Hermógenes Oliveira
> Prezados,
Olá, Alexandre.
> Estamos fazendo vários experimentos com a SUMO [1], sua tradução para
> TPTP/FOL [2] e verificação automática em provadores como E, Vampire
> etc. Estamos reportando várias inconsistencias [3] e dificuldades de
> obter provas que deveriam ser simples como o exemplo de Banana Slug
> [4].
>
> Em especial, estou procurando agora boas ferramentas interativas que
> aceitei como entrada TPTP, debugar provas longas de refutação não é
> tarefa fácil... Dicas? Alguém conhece algo pronto?!
tenho alguma experiência com o formato TPTP/ILTP.
Se entendi bem o que você precisa, tenho algumas informações que possam
ser relevantes.
Primeiro, baseado numa rápida passada de olhos, me parece que para
resolver o Banana Slug não basta lógica de primeira ordem (TPTP-FOF),
mas é necessário lógica de ordem superior (TPTP-THF)[1].
Quanto a assistentes interativos que trabalhem com o formato TPTP, sei
que o Isabelle contém uma ferramenta tptp_isabelle e que o Matita também
seria capaz de trabalhar com TPTP.
Porém, embora já tenha usado tanto Isabelle quanto Matita, nunca
trabalhei neles com problemas no formato TPTP. Portanto, não sei dizer
se o suporte para TPTP está limitado a FOF ou inclui a extensão para
ordem superior THF.
Dê uma olhada no SystemonTPTP do Prof. Sutcliffe[2]. Talvez encontre
ali no meio um ATP/ITP que satisfaça suas demandas.
Saudações,
Notas:
[1] Imagino que funções indutivamente definidas são necessárias para a
parte aritmética, não?
[2] http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTP
--
Hermógenes Oliveira
Reply all
Reply to author
Forward
0 new messages