P R O T O C O L (Michael)
                   17th September 2002, Castellon
              Working session: Dealing with rest of WP4





/--------------------------------------\
| Structure and content of deliverable |
\--------------------------------------/

1. Summary
  * Considered 2 protocols
  * n properties
  * m verified
  * k problems
  * i confirmed
  => verification is relevant and beneficial
  What is the benefit?

  Example: Verification showed that Indicator 7 is valid only under assumptions

  Big items:
  * It uncovered flaws
  * It was harder than expected

2. Verification of Jaundice
  For each property:
  * Informal explanation of property
  * Significance/Role of property
  * Considered further? If no, why?
  * If yes, formalisation
  * Summary of proof
  * Result

  One proof in detail => Indicator (somehow self contained paper, Appendix B)

3. Verification of Diabetes
  For each property:
  * Informal explanation of property
  * Significance/Role of property
  * Considered further? If no, why?
  * Result

4. Spin-Offs
  * KIV improvements
    - Fine tuned rules
    - Heuristics
  * Formalisation improvements
    - Patterns for Asbru plans
      => More automatic translation next time
    - Patterns for Intentions

5. Future challenges
  * Proof strategy
    - Lemma generation
    - Problems

Appendix
A Proof protocol for example proof
B Report on verification of Indicator
  - Jaundice
  - MAJIC indicator
  - Formalization (protocol and property) (one example, reference to EKAW)
  - Proof attempt(s)
  - Lessons learned
  - Future improvements