Existe-t-il un système de preuve automatisé raisonnable pour les théorèmes TCS?

28

Supposons que je veuille formaliser la preuve de Turing concernant le problème d'arrêt pour qu'une machine puisse le vérifier. Certains des systèmes de démonstration de théorèmes automatisés bien connus incluent Mizar, Coq et HOL4. J'ai téléchargé et expérimenté avec Coq, mais il n'a pas de bibliothèque pour les machines Turing. J'ai pensé à en coder un moi-même, mais j'ai trouvé le tutoriel manquant et la langue difficile à comprendre.

Ma question est la suivante: existe-t-il un prouveur de théorèmes automatisé qui est généralement bon pour prouver des théorèmes impliquant des machines de Turing? Je considérerais un tel prouveur de théorèmes comme «bon» s'il peut formaliser une preuve de l'indécidabilité du problème d'arrêt à l'aide de bibliothèques déjà existantes. Je le considérerais encore mieux s'il est relativement facile à ramasser. (Pour mémoire, je n'ai généralement pas de difficulté avec les langages de programmation.)

Merci,

Philippe

lo.logic turing-machines software proof-assistants automated-theorem-proving Philip White
la source
Vous voudrez peut-être vérifier cette page, mais la liste n'inclut pas le problème d'arrêt.
Kaveh
10
J'ose dire que vous devez persister avec quelque chose comme Coq avant qu'il ne semble naturel. Et vous devez être au terminal pour résoudre les problèmes, plutôt que de lire le livre. Il vous sera utile de mettre la main sur "Preuve de théorèmes interactifs et développement de programmes: Coq'Art: le calcul des constructions inductives". Tutoriels Coq: cis.upenn.edu/~bcpierce/sf et adam.chlipala.net/cpdt sont assez bons (bien qu'ils ne visent pas directement ce que vous voulez).
Dave Clarke
5
La formalisation d'une preuve peut être assez compliquée si vous en choisissez la "mauvaise" version. Pour le problème de l'arrêt, je suggérerais de prouver d'abord une version plus générale et abstraite. Ensuite, vous pourrez prouver plus tard que les machines Turing sont un cas particulier de la version abstraite, si vous avez toujours envie de le faire (il y aura beaucoup de détails fastidieux sur les machines Turing, alors peut-être qu'il serait préférable de consacrer du temps à faire autre chose). Je réfléchirai à un bon moyen de le prouver dans Coq. Resté à l'écoute.
Andrej Bauer
5
Si vous êtes bon en mathématiques et en programmation, vous avez les prérequis pour apprendre à utiliser un assistant de preuve. Vous devez vraiment la traiter comme une nouvelle compétence. (C'est cependant très gratifiant.)
Neel Krishnaswami
Il semble que la réponse à la question soit «non». Un tel système serait très utile je pense - puis-je demander que si vous formalisez des machines de Turing, pourriez-vous réfléchir à l'équivalence polynomiale?
Colin McQuillan

Réponses:

17

Voici une bibliothèque Isabelle / HOL contenant le théorème de Rice, qui indique l'indécidabilité d'un large éventail de problèmes. Étant donné que cette bibliothèque modélise la calculabilité via des fonctions récursives, vous devez coder une machine Turing universelle en tant que fonction récursive afin d'utiliser ce théorème pour prouver l'indécidabilité du problème d'arrêt des machines Turing. Cependant, les parties essentielles de la preuve de l'indécidabilité sont déjà terminées.

http://afp.sourceforge.net/browser_info/current/HOL/Recursion-Theory-I/index.html

yhirai
la source