O software existe para validar automaticamente um argumento?
Eu gostaria de
- Derive argumentos lógicos do inglês, e
- testar sua validade usando um programa.
Existe software para a etapa 2? Seria bom se fosse desistir porque
- A validade não é computável, ou
- levaria muito tempo para relatar um resultado.
Sei que fazer essa pergunta pode revelar minha ignorância sobre a lógica, então, se for uma pergunta boba, ficaria grato por algumas referências que explicam o porquê. Vou começar com Metalogic: Uma Introdução à Metateoria da Primeira Ordem Padrão .
Respostas
Você está procurando um assim chamado provador automatizado de teoremas .
Veja, por exemplo, pyPL ou Tree Proof Generator para duas implementações do cálculo de tableaux analíticos para a lógica proposicional clássica e lógica de primeira ordem.
O cálculo do tableau está completo para validade de primeira ordem, o que significa que toda inferência válida será detectada como tal.
Mas a lógica de primeira ordem não é co-semidecidível, o que significa que é impossível encontrar um algoritmo que detecte todas as não inferências como tais; em algumas inferências inválidas, o algoritmo do tableau será executado no infinito.
A lógica proposicional, por outro lado, é totalmente decidível; o algoritmo do tableau eventualmente detectará todos os argumentos proposicionais válidos e inválidos como tais.
Também existem restrições de complexidade; árvores de tableau são particularmente vulneráveis à explosão combinatória, a menos que heurísticas sofisticadas sejam implementadas, então os dois programas acima só funcionarão realisticamente para argumentos comparativamente simples.
Implementações de muitos outros sistemas de prova também foram feitas. A Wikipedia lista um monte, mas eu não trabalhei com nenhum deles, então você terá que verificar quais deles são adequados para casos de uso não acadêmicos e não industriais.