MathemaTeX

[projetmbc]

Bonjour,
je voudrais tenter de faire un prog. pour rechercher des démonstrations automatiques SIMPLES pour la Géométrie ou pour la résolution de petits problèmes d'Analyse.
Il existe des projets performants en Géométrie mais bon j'ai envie de m'essayer à cela.

QUESTION : quel langage se prête bien à ce genre de choses ? J'ai entendu parler de prolog. Quel est son intérêt par rapport à d'autres langages ?

[Arnaud]

SciPy ne convient pas ? ( je n'ai pas testé ).

[François D.]

Je n'ai pas bien compris de quoi tu voulais parler, mais je peux te donner quelques informations sur le langage Prolog.

Ce langage est dit déclaratif : on ne dit pas comment résoudre un problème (via un algorithme, etc.), mais à quelle condition on le considère comme résolu.

Liens : http://fr.wikipedia.org/wiki/Langage_de_programmation (généralités sur les types de langages)
http://fr.wikipedia.org/wiki/Programmat ... 9clarative pour la notion de langage déclaratif
http://fr.wikipedia.org/wiki/Prolog pour Prolog lui-même

[projetmbc]

SciPy ne convient pas ? ( je n'ai pas testé ).

En fait je voudrais à partir d'un ensemble donné d'hypothèses savoir si on peut aboutir à une conclusion. On parle de démonstration automatique mais je n'aime pas ce terme car il est très trompeur.

Je n'ai pas bien compris de quoi tu voulais parler, mais je peux te donner quelques informations sur le langage Prolog.
Ce langage est dit déclaratif : on ne dit pas comment résoudre un problème (via un algorithme, etc.), mais à quelle condition on le considère comme résolu.

Cela a l'air intéressant. Merci pour les liens

Si certains se sont déjà posés la question sujet de ce post, je suis preneur de leur expérience.

[Aleph]

Bonjour,

ce logiciel peut peut-être t'aider http://www.lama.univ-savoie.fr/~RAFFALLI/phox.html.
Si tu cherches des conseils, je peux te donner les adresses des profs de logique que j'ai eu en dea (par message privé).
Ils pourront sûrement t'aider : ils proposaient des stages en démonstration automatique à l'époque.

[Garulfo]

Le logiciel que tu pointes est un assistant de preuve. Il ne fournit pas de preuve... quoi qu'il dispose de stratégie pour cela, comme Coq ou Isabel HOL. Mais la pratique montre que tu as intérêt à savoir démontrer ce que tu espères que l'assistant t'aide à démontrer. Il me semble que l'auteur voulait — dans un temps fort fort lointain — un outil qui lui donnait une preuve. C'est un problème autrement plus complexe. Travailler avec Rodin et Event-B offrirait de meilleurs résultats probablement. Prolog ne remplissait pas plus les critères d'ailleurs. La programmation déclarative logique résoud des contraintes mais ne donne pas de démonstration.

Maintenant j'ai peut-être mal compris et puisque le fil est mort depuis longtemps nous ne le saurons peut-être jamais ^_^

[projetmbc]

...comme Coq ou Isabel HOL...Travailler avec Rodin et Event-B offrirait de meilleurs résultats probablement.

De nouvelles références... Super. Quant à la méthode, je ne me suis pas encore vraiment penché dessus étant donné que je vais être limité par le logiciel que je vais utiliser.

Ceci étant dit, je vais m'attaquer à des choses de niveau Lycée, ceci ne devrait pas être violent à faire.

[Garulfo]

Ah bin... si tu es là et que tu suis, expliques moi plutôt précisement ce que tu cherches.
Coq, HOL et phox sont des logiciels puissants mais qui nécessite de bien s'y connaitre avant de pouvoir se lancer — quoiqu'en dise à chaque fois les auteurs —. Le B est un peu plus à portée je pense... d'un professeur ou d'un étudiant en mathématique, mais pas d'un élève de secondaire.

Donc tout dépend de tes besoins.

[projetmbc]

Ah bin... si tu es là et que tu suis...

Oui, oui, il m'arrive de quitter le devant de mon écran.

...expliques moi plutôt précisement ce que tu cherches.

J'ai deux buts :

• Le premier est de me faire un outil de démonstration automatique en géométrie 2D et 3D de niveau Lycée. L'idéal serait quelque chose qui fasse du pas à pas.
• Le second serait d'avoir un outil à disposition des élèves pour tester des conjectures géométriques. Ceci devrait être "plus simple" à faire. Mon prog. se chargerait d'appeler Coq, par exemple, et côté élève la syntaxe serait énormément simplifiée.

[Garulfo]

...expliques moi plutôt précisement ce que tu cherches.

J'ai deux buts :

• Le premier est de me faire un outil de démonstration automatique en géométrie 2D et 3D de niveau Lycée. L'idéal serait quelque chose qui fasse du pas à pas.
• Le second serait d'avoir un outil à disposition des élèves pour tester des conjectures géométriques. Ceci devrait être "plus simple" à faire. Mon prog. se chargerait d'appeler Coq, par exemple, et côté élève la syntaxe serait énormément simplifiée.

Tu parles de géométrie euclidienne pas cartésienne. Je veux dire que ce que tu cherches c'est une base axiomatique, un théorème et inférer automatiquement les déductions qui y mènent ? Ça se ferait bien avec Coq ça. Mais comme je te l'ai dit c'est un outil qu'il faut savoir utiliser. Entre autre, il n'y a pas de base de tiers exclus. On peut l'ajouter mais cela fait parti des choses destabilisantes. Ensuite il te faudra énumérer tous les axiomes que tu vas utiliser (tu prendras je suppose ceux des éléments) puis, pour une preuve automatique, monter les stratégies de preuve. C'est tough en tabarnak quand on ne s'y est jamais mis avant.

Pour une idée de ce que représente Coq : http://www.pps.jussieu.fr/~miquel/enseignement/mpri/

Heureusement pour toi il existe des choses déjà bien pensées :
http://www.activemath.org/workshops/Mat ... hUI07.html

Sinon tu peux toujours utiliser Coq en utilisant des théories déjà construites : http://coq.inria.fr/contribs/HighSchoolGeometry.html

C'est un beau projet que tu as là. Mais ça peut-être très difficile de le rendre utile car il te faudra aussi penser convenablement l'interface.

Bon courage en tout cas

[projetmbc]

Tu parles de géométrie euclidienne pas cartésienne.

Les deux sont envisageables.

Tu parles de géométrie euclidienne pas cartésienne. Je veux dire que ce que tu cherches c'est une base axiomatique, un théorème et inférer automatiquement les déductions qui y mènent ? Ça se ferait bien avec Coq ça. Mais comme je te l'ai dit c'est un outil qu'il faut savoir utiliser.

Je sais. J'ai investi dans ce livre.

Entre autre, il n'y a pas de base de tiers exclus.

On peut l'ajouter mais cela fait parti des choses destabilisantes.

Ouf.

Ensuite il te faudra énumérer tous les axiomes que tu vas utiliser (tu prendras je suppose ceux des éléments) puis, pour une preuve automatique, monter les stratégies de preuve. C'est tough en tabarnak quand on ne s'y est jamais mis avant.

Je sais, je prendrais le temps qu'il faut.

C'est un beau projet que tu as là. Mais ça peut-être très difficile de le rendre utile car il te faudra aussi penser convenablement l'interface.

C'est le moins difficile de mon point de vue.

[Garulfo]

Tu parles de géométrie euclidienne pas cartésienne.

Les deux sont envisageables.

Pas bien non. La géométrie cartésienne te posera le problème de la précision qui limite une approche mathématique de la géométrie (mathématique est opposé ici au monde réel qui est imparfait... si je peux m'exprimer ainsi).

Entre autre, il n'y a pas de base de tiers exclus.

On peut l'ajouter mais cela fait parti des choses destabilisantes.

Ouf.

C'est une base de logique intuitionniste. Cela permet de construire des programmes à partir des démonstrations. Ainsi Coq peut servir à créer des programmes qui sont assurés de respecter leurs spécifications. Ce travail utilise l'isomorphisme de Curry-Howard. Il est plus difficile d'automatiser des preuves en utilisant le tiers-exclu. Ce n'est pas le seul problème bien sûr.

C'est un beau projet que tu as là. Mais ça peut-être très difficile de le rendre utile car il te faudra aussi penser convenablement l'interface.

C'est le moins difficile de mon point de vue.

Détrompes-toi. C'est la partie la plus complexe en fait. À moins que tu ais des connaissances en créations d'IHM pour des logiciels scolaires. La création d'interface qui répondent à des impératifs éducatifs — par exemple, car on pourrait parler d'interface pour des utilisateurs déficients ou pour des vieilles personnes etc. — est un tâche extrêmement complexe. J'ai travaillé avec plusieurs projets qui avaient pour but de fournir des outils à des étudiants universitaires en info. Au final, ça a toujours posé problème au niveau de l'interface. Elle doit être simple, mais complète... indicative, mais non directive...

[projetmbc]

La géométrie cartésienne te posera le problème de la précision qui limite une approche mathématique de la géométrie (mathématique est opposé ici au monde réel qui est imparfait... si je peux m'exprimer ainsi).

Sauf si on utilise des bibliothèques de calcul formel...

C'est une base de logique intuitionniste. Cela permet de construire des programmes à partir des démonstrations. Ainsi Coq peut servir à créer des programmes qui sont assurés de respecter leurs spécifications. Ce travail utilise l'isomorphisme de Curry-Howard. Il est plus difficile d'automatiser des preuves en utilisant le tiers-exclu. Ce n'est pas le seul problème bien sûr.

Il va falloir que je me mette à niveau.

Détrompes-toi. C'est la partie la plus complexe en fait. À moins que tu ais des connaissances en créations d'IHM pour des logiciels scolaires. La création d'interface qui répondent à des impératifs éducatifs — par exemple, car on pourrait parler d'interface pour des utilisateurs déficients ou pour des vieilles personnes etc. — est un tâche extrêmement complexe. J'ai travaillé avec plusieurs projets qui avaient pour but de fournir des outils à des étudiants universitaires en info. Au final, ça a toujours posé problème au niveau de l'interface. Elle doit être simple, mais complète... indicative, mais non directive...

Je vais utiliser PyQt que je connais un peu, donc ce n'est vraiment pas cela qui m'effraie. De plus, pour les figures géométriques permettant de visualiser ce qu'il se passe, je vais "hacker" des logiciels libres comme CaRMetal donc je n'aurais pas grand chose à faire.