Discuter:Assistant de preuve

Un article de Wikipédia, l'encyclopédie libre.

	Assistant de preuve fait partie du projet Informatique, qui a pour but d'enrichir le contenu de Wikipédia sur les sujets liés à l'informatique. Si vous voulez participer, vous pouvez modifier cet article ou visiter la page du projet où vous pourrez vous joindre au projet et consulter la liste des tâches et des objectifs. Le portail informatique pourrait aussi vous intéresser.
Ébauche	Cet article a été classé comme d'Avancement ébauche selon le Tableau d'évaluation du projet. (Voir les statistiques)
Moyenne	Cet article a été classé comme d'Importance moyenne selon le Tableau d'évaluation du projet. (Contester?)

	Assistant de preuve fait partie du projet Mathématiques, qui a pour but d'enrichir le contenu de Wikipédia sur les sujets liés aux mathématiques. Si vous voulez participer, vous pouvez modifier cet article ou visiter la page du projet, où vous pourrez vous joindre au projet et consulter la liste des tâches et des objectifs. Le portail Mathématiques pourrait aussi vous intéresser.
Ébauche	Cet article a été classé comme d'Avancement ébauche selon le Tableau d'évaluation du projet. (Voir les statistiques)
À évaluer	Cet article a été classé comme d'Importance ? selon le Tableau d'évaluation du projet.

"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?

[modifier] 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

«prouveur interactif» qui est court et clair mais qui est un anglicisme assez peu utilisé à l'écrit.
«assistant de preuve» qui est pas mal mais je trouve que cela représente mal les prouveurs non-interactifs.
«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)

[modifier] 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)