Alexandre Rademaker <aradema...@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 -- 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+unsubscr...@dimap.ufrn.br. Para postar neste grupo, envie um e-mail para logica-l@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/87shwgnpuv.fsf%40camelot.oliveira.
