O software existe para validar automaticamente um argumento?

Dec 20 2020

Eu gostaria de

  1. Derive argumentos lógicos do inglês, e
  2. testar sua validade usando um programa.

Existe software para a etapa 2? Seria bom se fosse desistir porque

  1. A validade não é computável, ou
  2. 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

13 lemontree Dec 20 2020 at 22:34

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.