Groupe "au delà de l'algo-prog"

* on parle peu d'algorithmique distribué (et pourtant cela nous entoure)

Discussion à part sur une chimère “logique”

But

  • comprendre des spécifications pour faire la différence entre “pour tout x, il existe y, ….”, “il existe y, pour tout x, …”
  • savoir faire des preuves
  • comprendre la notion de “langage formel”
  • comprendre la notion de “boite noire” (théorème à utiliser)

Qui ?

  • école primaire : modus ponens “s'il pleut, je prends un parapluie. Comme il pleut, alors je prends un parapluie”.
  • collège : initiation aux démonstrations avec géométrie

Projet : outil pour construire des preuves niveau collège et lycée

  • pouvoir formaliser la conjecture à démontrer
  • dessiner des situations géométriques (comme cabrigraph et geogebra )
  • pouvoir manipuler / construire des preuves
  • il faut des retours du logiciel compréhensible pour l'élève
  • s'adapter au programe du collège et lycée, où il n'y a plus trop de démonstrations à produire
    • voir les programmes de maths
  • pouvoir évaluer des énoncés dans des situations concrètes
    • à la Tarski's world
    • pratique pour faire la différence entre “pour tout x, il existe y, ….”, “il existe y, pour tout x, …”
    • pt construire des preuves en vrai avec des briques des légos
    • des smartphones sur lesquels sont écrits des énoncés mathématiques que l'on peut placer sur des règles concrètes et ça produit de nouvelles formules

Comment ?

  • utiliser Coq ou pas
    • Coq lourd

Difficultés

  • Problème de l'implication
  • Ne pas venir avec notre “vocabulaire”
  • Venir avec quelque chose de proche d'eux
  • Difficulté pour les élèves de voir dans le plan / l'espace
  • inviter les profs à un workshop ?
    • les profs n'ont pas le temps :(
  • Evaluation pas faite par les profs mais on reccueille les données

Etat de l'art

Specification de l'outil

Justifications

  • compétences utilisées
    • description (ou fourniture) d'une scene geométrique en formules (specifications, modélisation) ou representation géométrique d'une specification
    • formulation (ou fourniture) d'une hypothèse a prouver (but)
    • direction d'un robot prouveur (fourniture d'indices, suivi de la visualisation de l'avancement de la preuve)

Autres idées

  • Décrire le niveau de jeu avec une formule logique (logique ATL pour décrire les scénarios possibles)