Démonstration calculée, quel langage utiliser ?

Discussions générales concernant les mathématiques et n'entrant pas dans les catégories suivantes.
[participation réservée aux utilisateurs inscrits]
Règles du forum
Merci de soigner la rédaction de vos messages et de consulter ce sujet avant de poster. Pensez également à utiliser la fonction recherche du forum.
projetmbc
Utilisateur chevronné
Utilisateur chevronné
Messages : 2238
Inscription : samedi 29 décembre 2007, 00:58

Démonstration calculée, quel langage utiliser ?

Message non lu par 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
Modérateur honoraire
Modérateur honoraire
Messages : 7097
Inscription : lundi 28 août 2006, 13:18
Localisation : Allemagne
Contact :

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

Message non lu par Arnaud »

SciPy ne convient pas ? ( je n'ai pas testé ).
Arnaud
Un peu d'info - Pyromaths - Pas d'aide en MP (non plus)
François D.
Utilisateur chevronné
Utilisateur chevronné
Messages : 1367
Inscription : dimanche 30 juillet 2006, 10:04
Localisation : Alsace

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

Message non lu par 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
Utilisateur chevronné
Utilisateur chevronné
Messages : 2238
Inscription : samedi 29 décembre 2007, 00:58

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

Message non lu par projetmbc »

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

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

Message non lu par 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

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

Message non lu par 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
Utilisateur chevronné
Utilisateur chevronné
Messages : 2238
Inscription : samedi 29 décembre 2007, 00:58

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

Message non lu par projetmbc »

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

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

Message non lu par 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
Utilisateur chevronné
Utilisateur chevronné
Messages : 2238
Inscription : samedi 29 décembre 2007, 00:58

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

Message non lu par projetmbc »

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

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

Message non lu par Garulfo »

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 ;)
projetmbc
Utilisateur chevronné
Utilisateur chevronné
Messages : 2238
Inscription : samedi 29 décembre 2007, 00:58

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

Message non lu par projetmbc »

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

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

Message non lu par Garulfo »

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...
projetmbc
Utilisateur chevronné
Utilisateur chevronné
Messages : 2238
Inscription : samedi 29 décembre 2007, 00:58

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

Message non lu par projetmbc »

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.
Répondre
  • Sujets similaires
    Réponses
    Vues
    Dernier message