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)

  • Decided what to say in Dream Talk*

  • Gave up on critic and decided to see if we could get IsaPlanner to do what it should do after the critic happened. Got part way through implementing this, then got stuck on the need to use Middle-Out Reasoning (which means leaving blank bits in your proof and filling them in later) because MJo (implementor of Middle-Out Reasoning in IsaPlanner had to go for circuit training).

  • More profitable discussions of proof specification languages - decided to try and write it up as a Blue Book Note** tomorrow.

  • Agreed on datatype axioms to be provided for TPTP THF. Also agreed I should email GS and CB to request a "datatype" keyword in TPTP THF.

  • Arranged to meet DA tomorrow afternoon.

  • Attended an informal talk on Qigong.

  • Following an emergency email, phoned G.'s school to say that her father had sprained his ankle (tackling his PhD student during a football game) so if an entirely strange man turned up to collect her he should not be treated as a pedophile of any description, only to find that B. had managed to get their phone number after all and had already spoken to them.

  • Phoned home to a conversation that included such choice gems as "I told G. I could pour her some orange juice but she'd have to come and collect it herself" and "I don't think I can manage to cook pasta for supper since I can't carry the saucepan". He said not to come home early, but then amended it to see how much pain he was in tomorrow morning.

To Do:

  • Write proof specification language stuff up as a Blue Book Note.

  • Get middle-out reasoning working in IsaPlanner.

* My description of a DReaM Talk has got lost in comments somewhere. It's a 90 minute talk in which the use of slides and projection equipment is discouraged but handouts are allowed. It's supposed to cover work-in-progress, or areas of current difficulty and audience participation is expected. It's called Dream because the Mathematical Reasoning Group occasionally fancifully refers to itself as the Discovery and Reasoning in Mathematics (DReaM) group.

** The Blue Book Note web page is also password protected so there is no point linking to it. They are a series of short notes on work in progress and are specifically for "epsilon-baked ideas where 0 < epsilon < 1". They are called Blue Book Notes after Wittgenstein's Blue Book in which he wrote lecture notes which (AB at least) asserts are frequently contradictory. These days the notes are also stored in a series of lever arch files. At the time of writing there are 1,627 of these of which I have written 42 - putting me 7th in the "who has written the most blue book notes" league table. However AB has written 433 so I'm not going to be topping that league table any time soon.

the current result of all the proof specification language discussions )
purplecat: Hand Drawn picture of a Toy Cat (Default)

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

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