Existe-t-il un logiciel qui utilise le format Fitch (utilisé dans Language, Proof and Logic), permet de mettre un ensemble spécifique de prémisses et d'objectifs et de nous montrer la liste complète des étapes nécessaires pour résoudre le problème?Fitch Format Proofs - Tous les solveurs automatiques autour?
Réponse courte: Non
Réponse moyenne: ne peut pas vraiment être fait, si l'on peut écrire un programme pour vérifier la validité d'une preuve donnée assez facilement. Dans le cas de la logique propositionnelle, le problème de trouver automatiquement une preuve est NP-complet (bien que décidable!), Et dans la logique du premier ordre, il y a de vrais théorèmes pour lesquels le prouveur ne s'arrêterait jamais. (indécidable) (via la preuve d'incomplétude de Gödel)
Si vous êtes intéressé à écrire une telle chose, vous pouvez essayer de le faire, et peut-être le faire fonctionner pour des cas plus petits, mais ce n'est pas faisable en général.
Si vous cherchez une telle chose pour obtenir des réponses à vos devoirs, arrêtez d'essayer. (a) vous ne le trouverez pas et (b) les problèmes de ce livre sont assez faciles, et peuvent être amusants! Essayez-les et demandez de l'aide si nécessaire. et, bien sûr, (c) vous n'apprendrez rien si vous trichez.
Tenir compte Apros par OLI Carnegie Mellon http://www.phil.cmu.edu/projects/apros/.
Bien que ce lien puisse répondre à la question, il est préférable d'inclure ici les parties essentielles de la réponse et de fournir le lien . Les réponses à lien uniquement peuvent devenir invalides si la page liée change. – honk
En fait, il existe des moyens mécaniques de générer des épreuves de style Fitch. Par exemple. le chapitre 13 du [manuel de logique de Paul Teller] (http://tellerprimer.ucdavis.edu/pdf/) contient une description d'une telle procédure pour la logique propositionnelle (en gros des arbres de vérité en notation Fitch). De plus, la logique du premier ordre est semi-déterminable, ce qui signifie qu'il existe des moyens de trouver mécaniquement une preuve si la suite est valide (bien que la recherche ne puisse jamais se terminer dans le cas d'un séquentiel invalide). Bien sûr, rien de tout cela n'est utile pour les devoirs logiques, puisque ces preuves ont tendance à être ridiculement longues ;-) –