This commit was manufactured by cvs2svn to create branch

[helm.git] / helm / papers / calculemus-2003 / outline.txt

diff --git a/helm/papers/calculemus-2003/outline.txt b/helm/papers/calculemus-2003/outline.txt
deleted file mode 100644 (file)
index 55cb826..0000000
--- a/helm/papers/calculemus-2003/outline.txt
+++ /dev/null
@@ -1,48 +0,0 @@
-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) Zack
-  Dettagli Implementativi
-  - codifica dello stato
-  - codifica dei suggerimenti
-  - registry del broker
-  - implementazione dei ws
-  - implementazione dei tutor (gen. automatica, 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