Edinburgh Day Four
Achieved:
To Do:
- Established that B. was well enough to get G. to school and can now walk without crutches. Re-assured that they won't starve before I get back I have stuck by my original plan to return home tomorrow evening.
- Talked to DA. This involved installing yet another version of emacs, a new version of proof general, three new versions of Isabelle and a new version of IsaPlanner and then patching the preferred configuration. Just got an email from DA asking rather plaintively if we could actually discuss research tomorrow rather than installation issues.
- Got IsaPlanner to perform a middle-out reasoning proof, but did this interactively and revealed a nice big search space. Agreed that since middle-out reasoning is a major part of MJo's thesis project she would look at the implications of handling the search space and I would carry on in interactive mode.
- Went to a talk on parallelising Computer Algebra - this won me a free lunch.
- Wrote a draft Blue book note on proof specification languages.
To Do:
- Integrate middle-out reasoning proof with a critic.
- Finish Blue book note.
- Get taken to dinner by group.