purplecat: Hand Drawn picture of a Toy Cat (Default)
100 Current Papers in Artificial Intelligence, Automated Reasoning and Agent Programming. Number 2

Jacob M. Howe and Andy King, A Pearl on SAT and SMT Solving in Prolog, Theoretical Computer Science Volume 435, 1 June 2012, Pages 43–55.
DOI: http://dx.doi.org/10.1016/j.bbr.2011.03.031
Open Access: Available from Kent School of Computing Publication Index: http://www.cs.kent.ac.uk/pubs/2012/3136/index.html

I'm not sure quite how the terminology of a programming pearl arose. It denotes a neat, elegant or otherwise illuminating solution to some programming problem. In this case the programming pearl shows how a solver for a certain sort of logic can be programmed up in only 22 lines of of the Prolog Programming language.

Details under the Cut )
purplecat: Hand Drawn picture of a Toy Cat (Default)
I have heard from the reviewers about the revised version of your
submission to JAR. Based on their comments,
I am happy to inform you that your submission is accepted provided the
following comments in the report can be addressed. Please prepare a
final version and send it to me along with a letter explaining how you
have handled the comments in the report. I will then decide and forward
the final manuscript to the publisher of JAR.

I have been trying to get this paper published in this particular journal since before G was born. I'm not sure quite when I started referring to it as the "Albatross Paper". My boss will be pleased as well. He's not one of the authors, but he'd like to help me improve my publication record and so clearly feels that telling me at regular intervals to get on with rewriting/resubmitting/chasing the progress of the thing is a duty. I'm sure it's a duty he'll be glad to be relieved of.

At this stage the research reported in the paper (an adaption of an automated reasoning technique called Rippling to a more expressive logic) is rapidly reaching the status of historic interest only. But it has irritated me somewhat to see the people currently using the technique, grappling with same problems I did a decade ago, without being able to do more than refer them to a technical report for solutions.

This entry was originally posted at http://purplecat.dreamwidth.org/937.html.
purplecat: Hand Drawn picture of a Toy Cat (proof planning)
If your proof plan is going astray,
with a wave-front blocking the way,
then dream up a lemma,
to ripple the fella,
so fertilize can have its day.

Alan Bundy

purplecat: Hand Drawn picture of a Toy Cat (ai)
When I ran the Automated Reasoning Workshop in 2006 I swore never to do so again. So I'm not quite sure how I ended up running it this year as well. It was a lot less stressful this time round, but then this time round I persuaded Volker Sorge to take responsibility for the finances and frankly running a workshop is a lot more fun if you don't have to worry about money. Volker was, in fact, running a big jamboree Conferences in Computer Mathematics and we just free-loaded on that in various ways. Volker was quite stressed.

The ARW is a slightly funny beast. Typically it runs on five minute talks and long poster sessions which is quite unusual for Computer Science conferences and workshops, at least, which tend to prefer full papers.

It also generally has several panel sessions which had Volker and I scratching our heads to think up topics. In the end I decided on a "Representation Panel", invited some people on it and then let them refine the topic to "It is impossible to automatically generate good representations for automated reasoning problems." This generated a lot of good discussion - representation always does because it is fascinating the way some problems become incredibly easy once you look at them the right way. A typical example is the so-called "mutilated checkerboard" problem. Imagine a square sub-divided into smaller squares (like a chess/checkerboard), now remove two diagonally-opposite corners - can the resulting board be covered by dominos (i.e. rectangles that will cover two of the small squares)?. The answer is "no" and the problem is made easy if you colour the checkerboard with alternating black and white squares, observe a domino always covers one black square and one white square and then observe that two diagonally opposite corners are always the same colour. Therefore there must always be either more black or more white squares. The representational trick is colouring the checkboard, representing it as black and white squares. If you do that the solution is much easier to find than if you don't. Of course its very difficult to see how you could automatically perform such representational tricks.

We managed to link up with the "Doctoral Consortium" for the second panel so we titled it "What should make successful research in Automated Reasoning" and then asked Simon Colton to chair it confident in the knowledge he would seize the opportunity to tell us we were doing it all wrong and, indeed, "no one real wants to prove theorems" was not long in coming. There were some interesting other points too. In particular Ullrich Hustadt asked why we were so bad, in Automated Reasoning, in building useable enduring artefacts - i.e. automated reasoners which more than one person could use and which had a shelf-life longer than a couple of years*.

The posters and meal also went well and the proceedings contained all the abstracts** so all in all I was happy. At the last minute, Volker subsidised the workshop meal for our funded students (we offer travel awards to students presenting posters at the workshop) so I deduce that the finances were looking good as well.

* Having built a couple of automated reasoners which only I could use and which rapidly became unusable to anyone I have some opinions on this, one of which is "never build an experimental system using an experimental programming language".

** something that went unaccountably wrong in 2006.


Aug. 15th, 2008 06:24 pm
purplecat: Hand Drawn picture of a Toy Cat (rippling)
I've this long list of things I've been meaning to blog about over the past few months. I recall making a rather drunken post from BundyFest at the time, but I thought I might try a more sober round up of the event. In brief, Alan Bundy, my PhD supervisor is 61 so we had a symposium to celebrate his 60th Birthday and the opening of the "Informatics Forum" - the rather fancy title of the new Departmental building created for Informatics in Edinburgh, after their previous department burned down in mysterious circumstances.

Alan has worked primarily in Automated Reasoning a field which, one the whole, I would say really took off in 1965 when Alan Robinson published "A Machine-Oriented Logic Based on the Resolution Principle". Alan Bundy started working in what was then the Metamathematics Unit at the University of Edinburgh in 1971 and this became a part of the the Department of Artificial Intelligence in 1974. It's worth remembering how young the field was at this time. Automated Reasoning was only 10 years on from its first major result (Robinson's Resolution paper mentioned above) and it was only 20 years since John McCarthy coined the term "Artificial Intelligence". So it's not surprising that Alan Bundy's early work also involved what are now considered separate subfields such as Machine Learning, Automated Software Engineering and Natural Language. At the symposium a number of his colleagues and students were invited to talk and they were spread across all these fields.

I would identify two major themes from the talks and panel sessions held at the symposium:

What happened to Strong General Artificial Intelligence )

Ontologies are the Grand Challenge )

Other interesting factlets:

Ewen MacLean wrote a Jazz piece based on rippling (probably Alan Bundy's most famous automated reasoning technique) which was performed by what, I gather, are some of Scotland's best Jazz musicians, at the reception. I don't pretend to understand how the music related to rippling though.

Everything was being filmed for posterity but that meant everyone taking the microphone to ask a question was supposed to identify themselves. Much amusement was thereby had every time Alan Bundy asked a question and started it by saying "I'm Alan Bundy".

Alan's PhD supervisor Reuben Goodstein was, in turn, supervised by Wittgenstein. I've always been rather pleased by the fact that, in PhD terms, I am a descendent of Wittgenstein and, of course, via Wittgenstien of Bertand Russell.

The most important thing Alan ever told me was that really intelligent people worry more about understanding things than looking stupid. Therefore they ask questions whenever they don't understand something. I'm not as good at this as I should be.
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)

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