helm/papers/calculemus-2003/outline.txt

   1 1) Zack, CSC
   2  Introduzione
   3   - web services
   4   - monet
   5   - svariati WS per CAS e TP
   6   - proof assistant
   7     - bassa automazione
   8     - application centric no client/server
   9     ==>> proof assistants come WS client
  10   - omega ants
  11 2) Zack
  12   Architettura
  13   - figura 7.1 mia tesi
  14   - attori (client, broker, tutor)
  15     - ruoli e funzionalita' di ognuno di essi (breve)
  16   - mapping con gli attori di monet
  17 3) Zack
  18   Dettagli Implementativi
  19   - codifica dello stato
  20   - codifica dei suggerimenti
  21   - registry del broker
  22   - implementazione dei ws
  23   - implementazione dei tutor (gen. automatica, thread)
  24 4) CSC
  25    Sample session
  26   - screen shot
  27 5) CSC
  28     Tutor implementati
  29   - stupidi
  30     - (1-1) con le tattiche del proof assistant
  31     - generazione automatica
  32   - searchPatternApply
  33 6) Conclusioni e sviluppi futuri
  34   - success story (gTopLevel)
  35     - tattiche pesanti
  36     ==>> distribuzione
  37     - scelta troppo larga per i neofiti
  38     ==>> suggerimenti
  39   - utile per power user (distribuzione)
  40   - utili per newbie (apprendimento)
  41   - sviluppi futuri
  42     - recursion?
  43     - rating dei risultati
  44     - risposte negative (disabilitare tattiche)
  45     - blackboard?
  46     - GUI
  47     - descrizione monet
  48     - uso di Mathematical Object Manager