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

  • 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.


  • 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)

  • 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.

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

  • Volunteered to give a Dream Talk on Friday

  • Printed out and read my papers on Program Slicing which I said I'd talk about in the Dream Talk

  • Long talk with LD about proof specification languages and control rules. Sent him draft paper on control rules by myself MJa and MP.

To Do:

Plan for Tomorrow:

  • AM: Work with MJo on writing proof critics in IsaPlanner.

  • PM: Prepare Dream Talk

  • Evening: Write more gibberish in my blog


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

April 2019

 1 234 5 6
7 8 91011 12 13
14 15 16 17 18 19 20


RSS Atom


Style Credit

Expand Cut Tags

No cut tags