Il n'existe pas de vrai prouveur automatique utilisable. Donc si on veut prouver des choses à l'aide de logiciels, on a deux choix:
- faire un prouveur automatique de trucs très simple ;
- faire un logiciel intéractif qui permet, avec le cerveau de l'utilisateur, de prouver des trucs compliqués.
Un assistant de preuve, c'est la seconde approche. Si tu veux montrer « A et B », il va te demander de prouver « A » puis de prouver « B ». Je connais des personnes qui font de la preuve d'algorithmes pour l'arithmétique flottante et avoir un logiciel qui « n'oublie pas » de cas, c'est précieux. Par ailleurs, un assistant de preuve permet de démontrer automatiquement des morceaux de preuves, ce qui rend la vie de l'utilisateur (un peu) plus facile.
# prouveur automatique/assistant de preuve
Posté par fmaz fmaz . En réponse au journal La preuve de programme : où en est-on ?. Évalué à 2.
- faire un prouveur automatique de trucs très simple ;
- faire un logiciel intéractif qui permet, avec le cerveau de l'utilisateur, de prouver des trucs compliqués.
Un assistant de preuve, c'est la seconde approche. Si tu veux montrer « A et B », il va te demander de prouver « A » puis de prouver « B ». Je connais des personnes qui font de la preuve d'algorithmes pour l'arithmétique flottante et avoir un logiciel qui « n'oublie pas » de cas, c'est précieux. Par ailleurs, un assistant de preuve permet de démontrer automatiquement des morceaux de preuves, ce qui rend la vie de l'utilisateur (un peu) plus facile.