Existe-t-il un logiciel pour valider automatiquement un argument?

Question

Je voudrais

1. Dérivez des arguments logiques de l'anglais, et
2. tester leur validité à l'aide d'un programme.

Existe-t-il un logiciel pour l'étape 2? Ce serait bien s'il abandonnait parce que

1. La validité n'est pas calculable, ou
2. il faudrait trop de temps pour signaler un résultat.

Je me rends compte que poser cette question peut révéler mon ignorance de la logique, donc si c'est une question idiote, je serais reconnaissant de quelques références qui expliquent pourquoi. Je vais commencer par Metalogic: une introduction à la métathéorie du premier ordre standard .

Answer 1

Vous recherchez un prouveur de théorème automatisé .

Voir par exemple pyPL ou Tree Proof Generator pour deux implémentations du calcul des tableaux analytiques pour la logique propositionnelle classique et du premier ordre.

Le calcul du tableau est complet pour une validité de premier ordre, ce qui signifie que chaque inférence valide sera détectée comme telle.
Mais la logique du premier ordre n'est pas co-semi-décidable, ce qui signifie qu'il est impossible de trouver un algorithme qui détectera toutes les non-inférences en tant que telles; sur certaines inférences non valides, l'algorithme de tableau fonctionnera à l'infini.
La logique propositionnelle, en revanche, est entièrement décidable; l'algorithme de tableau détectera finalement tous les arguments propositionnels valides et invalides en tant que tels.

Il existe également des contraintes de complexité; Les arbres de tableaux sont particulièrement vulnérables à l'explosion combinatoire à moins que des heuristiques sophistiquées ne soient implémentées, de sorte que les deux programmes ci-dessus ne fonctionneront de manière réaliste que pour des arguments relativement simples.

Des implémentations de nombreux autres systèmes de preuve ont également été réalisées. Wikipedia en énumère un tas, mais je n'ai travaillé avec aucun d'entre eux moi-même, vous devrez donc vérifier lesquels d'entre eux conviennent aux cas d'utilisation non académiques et non industriels.