Démonstration calculée, quel langage utiliser ?
Démonstration calculée, quel langage utiliser ?
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 ?
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 ?
-
- Modérateur honoraire
- Messages : 7097
- Inscription : lundi 28 août 2006, 13:18
- Localisation : Allemagne
- Contact :
Re: Démonstration calculée, quel langage utiliser ?
SciPy ne convient pas ? ( je n'ai pas testé ).
-
- Utilisateur chevronné
- Messages : 1367
- Inscription : dimanche 30 juillet 2006, 10:04
- Localisation : Alsace
Re: Démonstration calculée, quel langage utiliser ?
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
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
Re: Démonstration calculée, quel langage utiliser ?
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.Arnaud a écrit :SciPy ne convient pas ? ( je n'ai pas testé ).
Cela a l'air intéressant. Merci pour les liensFrançois D. a écrit :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.
Si certains se sont déjà posés la question sujet de ce post, je suis preneur de leur expérience.
Re: Démonstration calculée, quel langage utiliser ?
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.
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.
Re: Démonstration calculée, quel langage utiliser ?
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 ^_^
Maintenant j'ai peut-être mal compris et puisque le fil est mort depuis longtemps nous ne le saurons peut-être jamais ^_^
Re: Démonstration calculée, quel langage utiliser ?
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.Garulfo a écrit :...comme Coq ou Isabel HOL...Travailler avec Rodin et Event-B offrirait de meilleurs résultats probablement.
Ceci étant dit, je vais m'attaquer à des choses de niveau Lycée, ceci ne devrait pas être violent à faire.
Re: Démonstration calculée, quel langage utiliser ?
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.
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.
Re: Démonstration calculée, quel langage utiliser ?
Oui, oui, il m'arrive de quitter le devant de mon écran. :DGarulfo a écrit :Ah bin... si tu es là et que tu suis...
J'ai deux buts :Garulfo a écrit :...expliques moi plutôt précisement ce que tu cherches.
- 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.
Re: Démonstration calculée, quel langage utiliser ?
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.projetmbc a écrit :J'ai deux buts :Garulfo a écrit :...expliques moi plutôt précisement ce que tu cherches.
- 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.
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 ;)
Re: Démonstration calculée, quel langage utiliser ?
Les deux sont envisageables.Garulfo a écrit :Tu parles de géométrie euclidienne pas cartésienne.
Je sais. J'ai investi dans ce livre.Garulfo a écrit :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.
Garulfo a écrit :Entre autre, il n'y a pas de base de tiers exclus.
Ouf.Garulfo a écrit :On peut l'ajouter mais cela fait parti des choses destabilisantes.
Je sais, je prendrais le temps qu'il faut.Garulfo a écrit :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.
C'est le moins difficile de mon point de vue.Garulfo a écrit :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.
Re: Démonstration calculée, quel langage utiliser ?
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).projetmbc a écrit :Les deux sont envisageables.Garulfo a écrit :Tu parles de géométrie euclidienne pas cartésienne.
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.projetmbc a écrit :Garulfo a écrit :Entre autre, il n'y a pas de base de tiers exclus.Ouf.Garulfo a écrit :On peut l'ajouter mais cela fait parti des choses destabilisantes.
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 a écrit :C'est le moins difficile de mon point de vue.Garulfo a écrit :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.
Re: Démonstration calculée, quel langage utiliser ?
Sauf si on utilise des bibliothèques de calcul formel...Garulfo a écrit :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).
Il va falloir que je me mette à niveau.Garulfo a écrit :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.
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.Garulfo a écrit :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...
-
- Sujets similaires
- Réponses
- Vues
- Dernier message
-
- 1 Réponses
- 406 Vues
-
Dernier message par projetmbc
-
- 7 Réponses
- 1372 Vues
-
Dernier message par pzorba75
-
- 9 Réponses
- 1190 Vues
-
Dernier message par Amonbofis564
-
- 6 Réponses
- 1046 Vues
-
Dernier message par zazou
-
- 17 Réponses
- 1016 Vues
-
Dernier message par marco56