purplecat

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.

Achieved:

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

• Write an abstract to go with the title for my Dream Talk, decide what I'm going to say and prepare a handout.


• Try and find the beginnings of a Note JG and I started writing on proof specification languages and recall what we were thinking and how it relates to LD's work.


• Talk to LD about Induction Challenge Problems - in particular their specification in TPTP Typed Higher-Order Form.


• Implement at least one proof critic for program correctness in IsaPlanner.


• Talk to DA about implementing program slicing in ProofGeneral.

Plan for Tomorrow:

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


• PM: Prepare Dream Talk


• Evening: Write more gibberish in my blog