1) Zack, CSC
 Introduzione
  - web services
  - monet
  - svariati WS per CAS e TP
  - proof assistant
    - bassa automazione
    - application centric no client/server
    ==>> proof assistants come WS client
  - omega ants
2) Zack
  Architettura
  - figura 7.1 mia tesi
  - attori (client, broker, tutor)
    - ruoli e funzionalita' di ognuno di essi (breve)
  - mapping con gli attori di monet
3) Dettagli
  3.1) codifica dello stato e dei suggerimenti
    - oss: l'architettura e' generica non dipenda da una particolare codifica di
      dimostrazioni
    - interfaccia verso il broker
  3.2) client
    - proof assistant
  3.3) broker
    - registri
    - interfaccia verso i client (registrazione, sottoscrizione, state change,
      deregistrazione)
    - interfaccia verso i tutor (registrazione, suggerimento, deregistrazione)
  3.4) tutor
    - cosa puo' implementare un tutor
    - nessuna assunzione sulla correttezza del suggerimento
    - interfaccia verso il broker (start/stop musing)
    - thread (?)
4) CSC
   Sample session
  - screen shot
5) CSC
    Tutor implementati
  - stupidi
    - (1-1) con le tattiche del proof assistant
    - generazione automatica
  - searchPatternApply
6) Conclusioni e sviluppi futuri
  - success story (gTopLevel)
    - tattiche pesanti
    ==>> distribuzione
    - scelta troppo larga per i neofiti
    ==>> suggerimenti
  - utile per power user (distribuzione)
  - utili per newbie (apprendimento)
  - sviluppi futuri
    - recursion?
    - rating dei risultati
    - risposte negative (disabilitare tattiche)
    - blackboard?
    - GUI
    - descrizione monet
    - uso di Mathematical Object Manager