purplecat | Entries tagged with theorem proving:systems:isabelle

You're viewing

purplecat's journal
Create a Dreamwidth Account Learn More

Reload page in style: light

Achieved:

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.

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

May 2025

S	M	T	W	T	F	S
				1	2	3
4	5	6	7	8	9	10
11	12	13	14	15	16	17
18	19	20	21	22	23	24
25	26	27	28	29	30	31

Syndicate

Tags

100 papers [10]
absent friends [2]
academia [87]
- dead scientists [2]
- edinburgh informatics [3]
- groups
  - dream [2]
- impact [1]
- public understanding [28]
  - lego rover [21]
- publications [50]
- scientists
  - aaron sloman [1]
  - alan bundy [4]
  - douglas hofstadter [1]
  - john mccarthy [2]
- talks [22]
- teaching [1]
administrivia [1]
agents of shield [1]
ai [28]
- agents [24]
  - ail [9]
  - bdi [11]
    - goals [2]
  - groups [3]
  - languages
    - agentspeak [1]
    - oopl [1]
  - organisations [3]
- automated reasoning [7]
  - rippling [1]
  - sat [1]
  - smt [1]
- ethics [7]
- explainability [2]
- hybrid systems [1]
- knowledge representation [1]
- lego robots [1]
- planning [1]
- robotics [4]
aisb [10]
amazon [1]
anecdote [1]
arthuriana [6]
bernice summerfield [6]
- review [5]
birthday [11]
books [54]
- author
  - andrew cartmel [3]
  - ben aaronovitch [4]
  - c s lewis [1]
  - charlotte bronte [1]
  - craig hinton [2]
  - david mcintee [1]
  - david whittaker [1]
  - dorothy l sayers [1]
  - iain m banks [2]
  - ian rankin [2]
  - j r r tolkien [1]
  - jacqueline rayner [2]
  - jane austen [1]
  - jeff vandermeer [1]
  - jim mortimore [1]
  - jonathan blum [2]
  - justin richards [3]
  - kate orman [2]
  - kelly hale [1]
  - lance parkin [4]
  - lawrence miles [6]
  - mags halliday [5]
  - malcolm hulke [1]
  - marc platt [2]
  - mark michalowski [3]
  - mary stewart [1]
  - megan whalen turner [3]
  - michael moorcock [2]
  - neal stephenson [3]
  - paul cornell [4]
  - paul dale smith [5]
  - paul magrs [11]
  - philip purser-hallard [10]
  - phyllis ann karr [1]
  - rob shearman [3]
  - rosemary sutcliff [2]
  - sara paretskey [1]
  - shakespeare [1]
  - simon guerrier [2]
  - terrance dicks [2]
  - terry pratchett [1]
  - tolkien [3]
castle [1]
christmas [2]
class [7]
- review [7]
computer science [15]
- complexity theory [4]
- game theory [5]
  - economics [1]
- np problems [1]
- verification [3]
  - induction [1]
conferences [3]
- aamas [1]
- arw [1]
- clima [1]
conventions [6]
- eastercon [11]
  - 2010 [2]
  - 2011 [4]
  - 2012 [1]
  - 2015 [1]
  - 2025 [1]
- lass o gowrie [1]
crochet [40]
- amigurumi [11]
- garment [5]
- moogly cal [8]
- non-euclidean [10]
current events [24]
dark [1]
- icons [1]
diary [14]
doctor who [963]
- books [45]
  - annual [8]
  - cover [50]
    - benny adventure [1]
    - eda [4]
    - misc [9]
    - missing adventure [1]
    - new adventure [10]
    - nuwho [2]
    - pda [7]
    - target [16]
  - edas [2]
  - nas [4]
  - new series [9]
  - pdas [1]
  - storybook [1]
  - time and relative disse [5]
- comic [10]
  - fifth doctor [2]
  - first doctor [2]
  - fourth doctor [2]
  - second doctor [2]
  - sixth doctor [2]
  - third doctor [1]
- costume bracket [116]
- factsheet [1]
- fandom [2]
- fanzine [8]
  - channel d [1]
  - dwb [2]
  - skaro [1]
  - tides of time [1]
  - web planet [4]
- fiction [1]
  - martha [1]
  - thirteen [1]
  - yaz [1]
- icons [66]
  - ace [1]
  - adric [1]
  - amy+rory+river [1]
  - barbara [1]
  - barbara+ian [1]
  - ben [1]
  - bill+nardole+twelve [1]
  - chang lee [1]
  - cybermen [1]
  - dalek [1]
  - dan [1]
  - doctor+master [1]
  - dodo [1]
  - eight [1]
  - eleven [1]
  - eleven+river [1]
  - faction paradox [1]
  - fifteen [1]
  - four [1]
  - four+leela [1]
  - four+sarah [1]
  - fugitive doctor [1]
  - graham+ryan [1]
  - harry [1]
  - ian [1]
  - ice warriors [1]
  - jamie [1]
  - jamie+victoria [1]
  - jamie+zoe [1]
  - jo [1]
  - katarina [1]
  - leela [1]
  - liz [1]
  - mel [1]
  - nardole [1]
  - nyssa [1]
  - one [1]
  - osgood [1]
  - peri [1]
  - polly [1]
  - romana [1]
  - romana1 [1]
  - romana2 [1]
  - ruby [1]
  - sara [1]
  - sarah [1]
  - sarah+three [1]
  - sea devils [1]
  - seven [2]
  - shalka [1]
  - silurians [1]
  - six [1]
  - sontarans [1]
  - steven [1]
  - susan [1]
  - tegan [1]
  - tegan+turlough [1]
  - the master [3]
  - thirteen+yaz [1]
  - three [2]
  - turlough [1]
  - two [1]
  - unit [1]
  - vicki [1]
  - victoria [1]
  - yaz [1]
  - zoe [1]
  - zygons [1]
- new series [6]
- nuwho rewatch [72]
- paper dolls [79]
- picture [212]
  - ainley master [2]
  - alien [1]
  - amy [1]
  - amy/rory [1]
  - barbara [1]
  - behind the scenes [13]
  - bill [1]
  - bonnie langford [1]
  - cast [3]
  - clara [1]
  - convention [1]
  - daphne ashbrook [1]
  - david tennant [1]
  - delgado master [3]
  - donna [2]
  - dvd cover [5]
  - dwm [4]
    - cover [2]
  - eighth doctor [1]
  - eleventh doctor [3]
  - eleventh doctor episo [6]
  - elizabeth sladen [1]
  - exhibition [1]
  - fanart [8]
  - fifth doctor [4]
  - fifth doctor episode [7]
  - fiftheenth doctor epi [1]
  - first doctor [4]
  - first doctor episode [16]
  - fourth doctor [5]
  - fourth doctor episode [7]
  - frazer hines [2]
  - fugitive doctor [1]
  - india fisher [1]
  - jamie [4]
  - jo [3]
  - joanna lumley [1]
  - jodie whittaker [4]
  - k9 [1]
  - leela [2]
  - martha [3]
  - matt smith [1]
  - mickey [1]
  - missy [1]
  - monster [13]
  - new adventures [1]
  - nicholas courtney [2]
  - nicola bryant [1]
  - ninth doctor [1]
  - ninth doctor episode [1]
  - patrick troughton [1]
  - paul mcgann [1]
  - pearl mackie [2]
  - peri [2]
  - peter capaldi [1]
  - production team [1]
  - puzzle [1]
  - river song [1]
  - romana [3]
  - romana 1 [1]
  - romana 2 [2]
  - rose [3]
  - rowan atkinson [1]
  - russell t davies [1]
  - sara [1]
  - sarah [4]
  - second doctor [6]
  - second doctor episode [7]
  - seventh doctor episod [6]
  - shalka doctor [1]
  - sixth doctor [5]
  - sixth doctor episode [4]
  - susan [1]
  - sylvester mccoy [2]
  - tardis [3]
  - tegan [2]
  - tenth doctor [2]
  - tenth doctor episode [9]
  - the brigadier [1]
  - the master [3]
  - theatre [2]
  - third doctor [5]
  - third doctor episode [2]
  - thirteenth doctor [2]
  - thirteenth doctor epi [2]
  - tom baker [2]
  - turlough [1]
  - tv movie [1]
  - twelfth doctor episod [3]
  - unit [1]
  - vicki [1]
  - victoria [3]
  - villain [1]
  - web planet [2]
  - william hartnell [2]
  - yaz [1]
  - zoe [1]
- rec [1]
- review [428]
  - book [34]
    - non-fiction [7]
  - film [1]
  - tv [394]
    - classic [150]
    - new new series [10]
    - new series [233]
- russell davies [3]
- steven moffat [2]
- the randomizer [152]
- verity podcast [1]
- whordle [4]
dolls [78]
- lego [5]
  - nasa [3]
- paper dolls [79]
dreamwidth [3]
edinburgh [8]
- festival [1]
exercise [18]
- running [37]
  - london marathon [19]
facebook [5]
faction paradox [3]
- review [3]
family [12]
- b [23]
  - animals [1]
  - dinosaurs [16]
  - fossils [4]
  - media stardom [19]
- cousins [1]
- days out [1]
- g [4]
  - school [1]
fandom [3]
fandom friday [2]
fandom stocking [1]
fanfiction [3]
feminism [5]
films [8]
follow friday [7]
food [51]
- heston blumenthal [1]
- recipe [40]
fools and heroes [11]
fossil friday [54]
friends [2]
genealogy [16]
granny's diary [5]
grimm [1]
- icons [1]
history [4]
holidays [57]
- cleveland way [5]
- cornwall [3]
- hadrian's wall [23]
- orkney [13]
- ridgeway [3]
- scotland [2]
- snowdonia [5]
- wales [2]
- west highland way [9]
house [16]
i have no tag for this [24]
i saw this last week [107]
icons [43]
- castle [1]
- ladybird books [1]
iris wildthyme [5]
- review [4]
jobs [3]
kin-strife [10]
linkspam [21]
livejournal [14]
lizzie bennet diaries [1]
mathematics [21]
- formal proof [1]
- logic [1]
- non-euclidean [10]
- philosophy [6]
  - proof [2]
- verification [1]
mcu [2]
- icons [1]
  - natasha [1]
media stardom [7]
meme [65]
meta [1]
model checking [4]
- systems
  - java pathfinder [3]
oxford [1]
performing [1]
- music [1]
philosophy [8]
- ai [2]
- ethics [2]
- mathematics [3]
picspam [102]
- castle [27]
- hobbit hole [6]
- house [2]
- prehistoric monument [93]
- roman remains [8]
- travel [57]
  - holidays [34]
  - work related [22]
pokemon go [2]
- icons [1]
primeval [59]
- fiction [1]
  - becker [1]
  - blade [1]
  - crossover [1]
  - lester [1]
  - ryan [1]
  - ryan/stephen [2]
- icons [4]
  - abby/ryan [1]
  - becker [1]
  - becker/lester [1]
  - becker/matt [1]
  - becker/ryan [1]
  - blade/lester [1]
  - claudia/lester [1]
  - connor [1]
  - connor/lester [1]
  - danny [1]
  - danny/ryan [1]
  - jess/ryan [1]
  - lester [1]
  - lester/ryan [1]
  - nick/stephen [1]
  - ryan [1]
- review [45]
programming [14]
- ail [1]
- languages
  - agentspeak [2]
  - jason [1]
  - java [5]
  - maude [2]
  - prolog [2]
projects
- eass [13]
- mcapl [13]
- platform grant [1]
- rais [2]
- verifiable autonomy [1]
- vps [2]
random doctor who picture [264]
random poetry [1]
rant [6]
reading listening watching [93]
rec [1]
- humour [1]
resolutions [14]
review [590]
- book [136]
  - non-fiction [37]
    - history [25]
      - science [9]
- comic [2]
- film [9]
- tv [409]
  - class [6]
  - internet [1]
  - merlin [2]
  - sarah jane adventures [5]
  - survivors [4]
roleplaying [24]
ros [1]
science [1]
science fiction [2]
science
- astronomy [1]
  - apod [1]
share
- twitter [2]
social networking [3]
- google+ [2]
- tumblr [1]
star wars [2]
- dolls [1]
  - lego [1]
the expanse [2]
- icons [1]
  - crew [1]
the prisoner [1]
- icons [1]
theorem proving [6]
- middle-out reasoning [3]
- proof planning [5]
  - critics [2]
  - rippling [3]
- proof specification lang [2]
- systems
  - isabelle [2]
  - isaplanner [4]
  - maude [1]
  - proof general [3]
- theory slicing [1]
- tptp thf [3]
throwback thursday [53]
- an oxford childhood [12]
- ancestors [3]
- arthurians [6]
- conventions [1]
- dad [3]
- docsoc [1]
- family [1]
- larp [3]
- oules [1]
- politics [1]
- running [1]
- wheatley [3]
tolkienery [7]
- fiction [1]
  - crossover [1]
  - sauron [1]
torchwood [5]
- review [13]
travel [65]
- commuting [2]
- work related [34]
traveller [6]
tv [29]
- blakes seven [1]
- buffy [1]
- firefly [2]
- sapphire and steel [1]
urban dead [5]
web stuff [1]
wierd spam [2]
world war z [1]
- fiction [1]
  - crossover [1]
writing [2]

Page Summary

Edinburgh Day Four
Edinburgh Day Two

Active Entries

Style Credit

Base style: Transmogrified by Yvonne
Theme: Sleeping Warrior by dancing_serpent

Expand Cut Tags

No cut tags