Discussion:Assistant de preuve

"Coq, de plus, a lui-même été prouvé dans Coq..."

En quoi ce fait constituerait t-il une preuve du bon fonctionnement de Coq?

Problème de terminologie

Suite à ma création de Démonstrateur interactif de théorèmes je pense que je vais rediriger la page vers ici (ou la supprimer qu'importe).

En fait quelqu'un avait remarqué dans la page spécification informatique que «prouveur» n'existait pas en francais et était du jargon. Le fond du problème est que j'hésite entre

1. «prouveur interactif» qui est court et clair mais qui est un anglicisme assez peu utilisé à l'écrit.
2. «assistant de preuve» qui est pas mal mais je trouve que cela représente mal les prouveurs non-interactifs.
3. «Démonstrateur interactif de théorèmes» qui est vraiment lourd, mais qui a le mérite d'être très explicite.

Outs 25 avril 2007 à 16:11 (CEST)

« Preuve » dans le sens de « démonstration » est aussi du jargon, mais la français est une langue qui évolue, et donc même si on n'aime pas ce terme, il est passé dans le langage courant des chercheurs et des praticiens. Quant à « prouveur », je pense en effet que c'est du jargon. Ceci dit, je ne te suis pas entre 2. et 3. Pierre de Lyon 25 avril 2007 à 21:26 (CEST)

«assistant à la preuve» ou «assistant de preuve» est le terme utilisé dans la littérature scientifique française, et cela ne concerne effectivement que les logiciels interactifs, car un assistant est forcément interactif puisqu'il est là pour assister et non pas faire à la place. Pour les logiciels automatiques, je connais moins, mais de toute façon ni «prouveur», ni «démonstrateur» n'existent à l'origine en français (en tout cas pas dans ce sens là), et j'imagine que ça n'existait pas non plus en anglais. 14 mai 2010 à 23:21

Ensuite en ce qui concerne «preuve», je ne crois pas du tout que ce soit un anglicisme qui nous viendrait de «proof» mais un terme de la logique qui désigne une famille d'objet bien définis, contrairement à «démonstration» qui désigne plutôt un processus qui va permettre d'aboutir au final à une preuve. Le verbe prouver et le mot preuve sont utilisé depuis très longtemps en français (peut-être même avant que prove soit utilisé en anglais, verbe qui a d'ailleurs deux participe passé: proved et proven) 14 mai 2010 à 23:21

Ton opinion montre clairement que nous sommes dans une phase d'évolution du langage, car dans les années 60, disons, on ne parlait pas de « théorie de la preuve », mais bien de « théorie de la démonstration » pour qualifier ce que faisait Gentzen, par exemple. Je me souviens d'un collègue qui avait été éduqué par des grands logiciens belges et qui essayait sans succès de lutter conte l'anglicisation du vocabulaire et donc vers le glissement vers le terme « théorie de la preuve », mais sans succès. Je partage son point de vue, mais je suis plus fataliste et accepte l'évolution de la langue. En revanche, en évoluant la langue s'est enrichie, car, comme tu l'indiques, nous, français, faisons une nuance que les anglophones ne font pas entre «preuve» (objet) et «démonstration» (processus). Dire qu'une preuve (une démonstration) est un objet mathématique est assez récent, car cela date de l'article d'Howard grosso modo. Si je me trompe sur ce point, je te serais reconnaissant de m'en apporter la preuve ( au sens usuel du terme)--Pierre de Lyon (d) 20 mai 2010 à 10:09 (CEST)

L'article preuve du dictionnaire du CNTRL rappelle que preuve a un sens en mathématique qui n'est absolument pas celui dont tu parles et qui apparait dans preuve par neuf. --Pierre de Lyon (d) 20 mai 2010 à 10:14 (CEST)

Et les prouveurs automatiques ?

Je ne comprends pas pourquoi "Démonstration automatique" renvoit sur cette article, vu que les prouveurs interactifs et les prouveurs automatiques sont deux champs bien distincts du domaine. steki-kun 10 mai 2007 à 18:58 (CEST)

Je pense que tout le monde est d'accord la dessus. Mais le travail reste à faire voila tout :-) Outs 11 mai 2007 à 08:23 (CEST)

Ah ok :-) ben alors je vais ptet penser à traduire en:Automated theorem proving... mais cet article ne parle pas du tout des prouveurs SMT et des procédures de décision. steki-kun 11 mai 2007 à 10:32 (CEST)

J'ai commencé l'article démonstration automatique de théorèmes. Pierre de Lyon (d) 27 décembre 2007 à 23:12 (CET)

page a fusionner ici ?

Système de preuve interactive, en plus elle est brouillonne.Outs (d) 27 février 2009 à 16:05 (CET)

Oui la page est brouillone et incomplète, mais non ça n'est pas du tout la même chose, il s'agit d'un faux ami. Il ne faut surtout pas fusionner. Pierre de Lyon (d) 2 mars 2009 à 22:04 (CET)

A propos de la conjecture de Kepler

La phrase "1989 le problème n’est pas encore démontré complètement" paraît un peu périmée. Du moins, Thomas Hales prétend que la conjecture de Kepler est démontrée (Annals of Math. 165 (2002)) et que la preuve est certifiée (avec plusieurs systèmes) (Notices AMS 55 (2008), voir http://www.ams.org/notices/200811/tx081101370p.pdf et Discrete Comput. Geom. 44 (2010)). --JerGer (d) 17 octobre 2012 à 15:19 (CEST)

La démonstration de Hales n'est pas encore validé à 100% mais seulement à 99%, voir Conjecture de Kepler [1]. Rabah201130 (d) Je fais beaucoup de fautes d'orthographe, merci de me les corriger 17 octobre 2012 à 16:52 (CEST)

Théorèmes à vendre

Outre l'intérêt douteux de la section Théorèmes à vendre (que je propose de supprimer, car je trouve cela scandaleux) il faudrait au moins indiquer à qui on peut acheter les théorèmes. Je voudrais savoir qui est prêt à vendre le patrimoine de l'humanité pour quelques livres sterlings. --Pierre de Lyon (d) 19 avril 2013 à 12:21 (CEST)

C'est dans la source (il faut d'adresser à Flaminia Cavallo, à l'université d'Edimbourg). Cela dit, je suis d'accord que cette section est sans pertinence : aucun livre, ou article, centré sur le sujet de l'article (les assistants de preuve) ne parle de cela. Et tout le monde a oublié cela depuis 2010, cela ne doit même plus être possible. A supprimer --Jean-Christophe BENOIST (d) 19 avril 2013 à 12:33 (CEST)

 Théorèmes prouvés avec des assistants de preuve

Les dates des démonstrations par assistants sont bizarres. --Pierre de Lyon (discuter) 17 juillet 2016 à 12:19 (CEST)