Démonstration calculée, quel langage utiliser ?

Discussions générales concernant les mathématiques.
[ce forum est modéré par les modérateurs globaux du site]
Règles du forum
Merci d'éviter le style SMS dans vos messages et de penser à utiliser la fonction Recherche avant de poster un message. Pour joindre des fichiers à vos messages, consulter ce sujet.
> Penser à utiliser le mode LaTeX (voir ici) afin de rendre vos formules plus lisibles.
> Pour obtenir de l'aide sur un exercice ou un problème, consulter cette section. (ce forum est destiné aux discussions plutôt théoriques)

Démonstration calculée, quel langage utiliser ?

Messagepar projetmbc » Dimanche 30 Août 2009, 10:12

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 ?
projetmbc
Péta-utilisateur
 
Messages: 1895
Inscription: Samedi 29 Décembre 2007, 00:58
Statut actuel: Actif et salarié | Enseignant

Publicité

Re: Démonstration calculée, quel langage utiliser ?

Messagepar Arnaud » Dimanche 30 Août 2009, 10:37

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

Un peu d'info - Pyromaths
LaTeX - Exemples de formules LaTeX

Pas d'aide en MP (non plus)
Arnaud
Modérateur
 
Messages: 7113
Inscription: Lundi 28 Août 2006, 12:18
Localisation: Allemagne
Statut actuel: Actif et salarié | Enseignant

Re: Démonstration calculée, quel langage utiliser ?

Messagepar François D. » Dimanche 30 Août 2009, 10:42

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
François D.
Téra-utilisateur
 
Messages: 1370
Inscription: Dimanche 30 Juillet 2006, 09:04
Localisation: Alsace
Statut actuel: Actif et salarié | Enseignant

Re: Démonstration calculée, quel langage utiliser ?

Messagepar projetmbc » Dimanche 30 Août 2009, 13:07

Arnaud a écrit: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.

Franç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.

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.
projetmbc
Péta-utilisateur
 
Messages: 1895
Inscription: Samedi 29 Décembre 2007, 00:58
Statut actuel: Actif et salarié | Enseignant

Re: Démonstration calculée, quel langage utiliser ?

Messagepar Aleph » Dimanche 14 Février 2010, 20:26

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.
Aleph
Hecto-utilisateur
 
Messages: 86
Inscription: Mardi 05 Janvier 2010, 16:38
Statut actuel: Post-bac | Doctorat

Re: Démonstration calculée, quel langage utiliser ?

Messagepar Garulfo » Mercredi 17 Février 2010, 06:53

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 ^_^
Garulfo
Kilo-utilisateur
 
Messages: 107
Inscription: Mardi 10 Juillet 2007, 19:49
Localisation: Sherbrooke, Québec, Canada
Statut actuel: Actif et salarié | Maître de conférence

Re: Démonstration calculée, quel langage utiliser ?

Messagepar projetmbc » Mercredi 17 Février 2010, 10:55

Garulfo a écrit:...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.
projetmbc
Péta-utilisateur
 
Messages: 1895
Inscription: Samedi 29 Décembre 2007, 00:58
Statut actuel: Actif et salarié | Enseignant

Re: Démonstration calculée, quel langage utiliser ?

Messagepar Garulfo » Mercredi 17 Février 2010, 22:23

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.
Garulfo
Kilo-utilisateur
 
Messages: 107
Inscription: Mardi 10 Juillet 2007, 19:49
Localisation: Sherbrooke, Québec, Canada
Statut actuel: Actif et salarié | Maître de conférence

Re: Démonstration calculée, quel langage utiliser ?

Messagepar projetmbc » Jeudi 18 Février 2010, 09:32

Garulfo a écrit:Ah bin... si tu es là et que tu suis...

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

Garulfo a écrit:...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.
projetmbc
Péta-utilisateur
 
Messages: 1895
Inscription: Samedi 29 Décembre 2007, 00:58
Statut actuel: Actif et salarié | Enseignant

Re: Démonstration calculée, quel langage utiliser ?

Messagepar Garulfo » Vendredi 19 Février 2010, 05:20

projetmbc a écrit:
Garulfo a écrit:...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 ;)
Garulfo
Kilo-utilisateur
 
Messages: 107
Inscription: Mardi 10 Juillet 2007, 19:49
Localisation: Sherbrooke, Québec, Canada
Statut actuel: Actif et salarié | Maître de conférence

Re: Démonstration calculée, quel langage utiliser ?

Messagepar projetmbc » Vendredi 19 Février 2010, 13:28

Garulfo a écrit:Tu parles de géométrie euclidienne pas cartésienne.

Les deux sont envisageables.

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.

Je sais. J'ai investi dans ce livre.

Garulfo a écrit:Entre autre, il n'y a pas de base de tiers exclus.

:shock:

Garulfo a écrit:On peut l'ajouter mais cela fait parti des choses destabilisantes.

Ouf.

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.

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

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.

C'est le moins difficile de mon point de vue.
projetmbc
Péta-utilisateur
 
Messages: 1895
Inscription: Samedi 29 Décembre 2007, 00:58
Statut actuel: Actif et salarié | Enseignant

Re: Démonstration calculée, quel langage utiliser ?

Messagepar Garulfo » Vendredi 19 Février 2010, 23:05

projetmbc a écrit:
Garulfo a écrit: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).

projetmbc a écrit:
Garulfo a écrit:Entre autre, il n'y a pas de base de tiers exclus.

:shock:
Garulfo a écrit: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.

projetmbc a écrit:
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.

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...
Garulfo
Kilo-utilisateur
 
Messages: 107
Inscription: Mardi 10 Juillet 2007, 19:49
Localisation: Sherbrooke, Québec, Canada
Statut actuel: Actif et salarié | Maître de conférence

Re: Démonstration calculée, quel langage utiliser ?

Messagepar projetmbc » Samedi 20 Février 2010, 09:52

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).

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

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.

Il va falloir que je me mette à niveau. :shock:

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...

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.
projetmbc
Péta-utilisateur
 
Messages: 1895
Inscription: Samedi 29 Décembre 2007, 00:58
Statut actuel: Actif et salarié | Enseignant


Retourner vers Tribune des mathématiques

 


  • Articles en relation
    Réponses
    Vus
    Dernier message

Qui est en ligne

Utilisateurs parcourant ce forum: Proximic [Spider] et 1 invité