Edinburgh Day Two

[louisedennis]

Achieved:

• JG sent me a PDF of our note on proof specification languages: read but not digested.
• Asked LD about putting induction challenge problems into TPTP THF - LD agrees with my approach. LD tried to check type definitions in IsaPlanner for me: "unfortunately most of my systems are halfway between broken and working... which means they're broken".
• Installed latest versions of both Isabelle and IsaPlanner.
• Installed Aquaemacs because LD's sml-mode doesn't work in xemacs on the Mac
• Worked out how to use IsaPlanner using Aqaemacs - it was about 3pm when we got to this point. Getting everything
  set up was slow work not helped by the fact LD had food poisoning and didn't appear until midday leaving MJo and I flailing around rather.
• Created a handout for my dream talk.
• Started writing a critic for IsaPlanner - stalled firstly because Isabelle won't let me use partial definitions in the simplifier and then later because there is no way to remove rules from IsaPlanner's wave rule database (which would bypass the simplifier). LD was about to start working on this when South Central Edinburgh blacked out. I'm now in an Internet cafe on the lighted side of Nicholson Street.
• Observed the introduction of new "stylish" furniture to the Dream group communal areas. Listened to the departmental administrator curse architects and various others compare the furniture unflatteringly to contemporary bars and airport lounges.
• Discovered that Appleton Tower has extremely poor emergency lighting in the stairwell.

To do:

• Still no sign of DA
• Decide what to say in my dream talk
• Actually Implement that critic
• Discuss proof plan specification languages further with LD.