Apprentissage

• Prend en entrée une proposition à prouver, un domaine, la facon dont quelqu'un l'a résolu

• ne renvoie rien

• Prend en entrée (la string correspondant à la proposition à prouver, une liste des domaines qu'on est succeptibles d'utiliser)
  

• Si Goldorak hésite entre plusieurs voies : Renvoie Choose, un identifiant du problème, une description de ce qu'il a fait jusque là, ainsi qu'une liste de plan d'actions. L'identifiant permettra à Goldorak de retrouver le problème en question dans ses données, vu qu'il est succeptible de gérer plusieurs théorèmes successifs. Le taupin peut bien mettre de côté un exo.
  

• Si Goldorak s'engage dans une voie, mais tombe sur un os -> Renvoie Help, un identifiant du problème, une description de ce qu'il a fait pour l'instant, ainsi que la situation dans laquelle il bloque (la tête est la propriété à prouver, la queue les hypothèses).
  

• Si Goldorak est assez fort, il renvoie Completed, un identifiant du problème, la déscription "en français" de ce qu'il a fait, la liste de tactiques qui répond au problème ["simpl"; "rewrite H"; "reflexivity"; "trivial"]

(permet de reprendre la démonstration d'un théorème interrompu parce que Goldorak hésitait. L'utilisateur lui donne une indication)


• Prend en entrée une liste de booléens. Ces booléens sont des réponses que l'utilisateur fait à Goldorak. (si on veut donner plus de possibilités à l'utilisateur, ça peut être des entiers).
  

• Les réponses ont la même signification que les réponses de GoldorakGo

• Donne une liste de theoreme/tactiques a utiliser, une liste de buts intermediaires
  

• Les réponses ont la même signification que précédemment

Main : GoldorakGo (converge_serie (-1)^{n[n+ 5*cos n]/n}2) [serie]
-> (132, , " critère des série alternées")

Main : GoldorakChoose (132, [True,False])
->(132, n/n^2 decroissant?)

Main : GoldorakHelp (132, [simplificationQuotient; 1/n^{i decroissant], [n/n}{2} = 1/n])

• Choisir le/les manières générales dont va marcher l'apprentissage (par réseau de neurones? système expert? reconnaissance d'une classe de langage? ,...) : jeudi 8 octobre
  

• Choisir le langage dans lequel on implante ça : samedi 10 octobre
  

• Rendre une première version conne mais qui ne bugge pas : 8 novembre
  

• Rendre quelquechose de potable : 2 semaines avant date finale