purplecat: Hand Drawn picture of a Toy Cat (Default)
Achieved:

  • Gave Dream Talk. AB suggested checking out Machine Learning literature and asking AI about testing.

  • Got an IsaPlanner critic to work, but couldn't integrate it with the middle-out reasoning proof of yesterday.



Unachieved:

  • Blue book note still unwritten but exists as a draft.

  • End-to-end example of using program slicing to detect and error and then middle-out reasoning to fix it in IsaPlanner.

  • Any work with Proof General.



So all in all, not bad for five days. However its all likely to go on a back-burner now since, as AB says, my proof planning work is a hobby these days. So whether I'll be able to build on the achievements is unclear.
purplecat: Hand Drawn picture of a Toy Cat (Default)
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.

Profile

purplecat: Hand Drawn picture of a Toy Cat (Default)
purplecat

September 2017

S M T W T F S
     1 2
3 4 5678 9
10 11 12 131415 16
171819 202122 23
24252627282930

Syndicate

RSS Atom

Tags

Style Credit

Expand Cut Tags

No cut tags