¿Existe software para validar automáticamente un argumento?

Question

Me gustaría

1. Derivar argumentos lógicos del inglés y
2. probar su validez usando un programa.

¿Existe software para el paso 2? Estaría bien si se rindiera porque

1. La validez no es computable o
2. tomaría mucho tiempo informar un resultado.

Me doy cuenta de que hacer esta pregunta puede revelar mi ignorancia sobre la lógica, así que si es una pregunta tonta, agradecería algunas referencias que explican por qué es así. Voy a empezar con Metalogic: Introducción a la metateoría del primer orden estándar .

Answer 1

Está buscando el llamado demostrador de teoremas automatizado .

Consulte, por ejemplo, pyPL o Tree Proof Generator para ver dos implementaciones del cálculo de cuadros analíticos para la lógica proposicional clásica y de primer orden.

El cálculo del cuadro está completo para la validez de primer orden, lo que significa que cada inferencia válida se detectará como tal.
Pero la lógica de primer orden no es codecisible, lo que significa que es imposible encontrar un algoritmo que detecte todas las no inferencias como tales; en algunas inferencias no válidas, el algoritmo del cuadro se ejecutará hasta el infinito.
La lógica proposicional, por otro lado, es completamente decidible; el algoritmo de tableau eventualmente detectará todos los argumentos proposicionales válidos e inválidos como tales.

También existen limitaciones de complejidad; Los árboles de tableau son particularmente vulnerables a la explosión combinatoria a menos que se implementen heurísticas sofisticadas, por lo que los dos programas anteriores solo funcionarán de manera realista para argumentos comparativamente simples.

También se han realizado implementaciones de muchos otros sistemas de prueba. Wikipedia enumera un montón, pero no he trabajado con ninguno de ellos, por lo que tendrá que verificar cuáles son adecuados para casos de uso no académicos y no industriales.