Thursday, February 24, 2005

Software for OS X

GNUPlot (needs AquaTerm)
O'Caml
Graphviz

I've been playing with some Open Source software for OS X lately. There are links above, and brief descriptions follow.



GNUPlot is everybodies favourite graph plotting software. At the link above, you can download a version compiled for OS X against AquaTerm, a package that allows gnuplot to draw to a native window under Aqua.

O'Caml, is an object-oriented functional programming language in the ML family. I'll be working with it this year. From the official download page (linked above) you can get source distributions, or pre-compiled binary packages for many platforms, including OS X.

Graphviz is a package for drawing diagrams of graphs and networks. The link above, is for an excellent OS X port of graphviz with a document-based GUI and support for lots of output format. It won a couple of awards and the OS X port, and Grapviz itself, is open source.



I'll post links to some more useful OS X software later on.

Wednesday, February 23, 2005

On (or rather next to) my iPod

iPod Note Reader User Guide (PDF)

The other week, I bought myself a new iPod (and iWork) from my local Apple shop. Today I was poking around Apple's site and decided to see if they had an SDK of any description for the iPod. Apparently they do not, but I did find the user guide for the Notes application. It looks like you can get it to do some pretty cool tricks. When I get the time, I'll have a go at knocking together a bit of a demo of the sorts of things it can do, maybe set a short story to music and sound effects or some such, like those children's books with little icons in the text which cue the child to press the appropriate button to get a sound effect.

I'm not sure I understand the reasoning behind using XML for some of that stuff, but it's their product after all, so they can engineer it anyway they like. All we have to do is buy them... :-)

And so it beings...

On Friday, Pietro gave me a few papers and chapters to read regarding the theoretical aspect of my Honours project: techniques for extracting counter-models from open tableaux and implementing these techniques (or at least support for them) in the Tableau Work Bench. I've just finished my first reading of the first of these papers, and I'll note some points below.



I've just gone over the research report A tableau system for modal logic S4 with an efficient proof-search procedure by Toshimasa Matsumoto. It will take a few more readings (both of the paper itself and of those it references) before I get most of it, but it seems quite cool. As I understand it, the basic idea is to use the histories to prevent re-application of formulae and the attendant loops. This is quite straight forward. The bits I am still trying to wrap my head around are the way the tableau rules for CS4 accomplish this. I think that I've nearly got it worked out in my head, I just need to think about it a bit more.

What happens is applying rule (T) takes Γ, α to Γ, α, α and does not modify the history. When the transitional rules, (S4)s and (S4)t are applied, the α is converted back to α and is recorded in the history iff the current history is strictly smaller (i.e. subset but not equal to) than the history with α added to it, i.e. the history does not already contain α. This is cool, and I almost understand how the tableau rules do it.

The (T) rule, unless I am completely wrong, replaces the tree rule I am familiar with. The (S4)s and (S4)t rules replace the rule I am familiar with. The (S4)s and t rules also keep track of the applied s by updating the history. This is somewhat the equivalent of ticking the , and noting a world for a in the system I learnt last year.

The completeness proof, proof of termination and time complexity analysis all look interesting, but the most important part of the paper, for my purposes, is the section on constructing counter-models from an open tableau. As well as being relevant to what I'll be working on, this section was easier to read, as its content was somewhat familiar.

PS: I have used ∇ above to stand in for the filled box used in the paper, primarily because I can't be bothered making an image of a black box. In addition, neither the ☐, nor the ◊ are all that appropriate either.

Friday, February 04, 2005

Things I hate about my Flatmate

Just found a piss funny 'blog via "Blogs of Note" on Blogger.com: Things I hate about my Flatmate.

Some More Comics

I posted the following on one of my other blogs:
Viper Comics: Dead@17: The Complete First Series
Aria Volume One
Remote Volume One

I've just been to the comic shop spending the money I should be saving for kitchenware and next weeks food (I'll have to cook my own meals after I move into B&G tomorrow). I got Dead@17: The Complete First Series, Aria Volume One and Remote Volume One.

I got Aria as the cover art reminded me a little of Yokohama Kaidashi Kikou (English Scanlation) as did the cover text. I've not read it yet, but a quick flick through has made me want to go back (though the shop'll be closed now) and buy the other two volumes although, now that I think about it, they only had the third on the shelf. If this book turns out to be anywhere near as good as YKK, I'll have to try an get some more of his work.

I haven't read Remote yet, but I chose it due primarily to the cover text and the colour section at the front (though a quick flick through the book cemented the decision). I usually like detective and police related anime and manga (series such as Spiral, Saint Tail and the various Patlabor films, books and series come to mind) so I don't think this is much of a gamble.

I have just finished reading Dead@17 and it has once again reminded me that the Japanese do not have a monopoly on great comics. I'm definitely going to be getting the rest of Dead@17 and sooner rather than later.

It looks like Impact are going to be getting hold of a large chunk of my disposable income in the immediate future.

Wednesday, February 02, 2005

More on the Seikai Trilogy

The Seikai Trilogy

I've just read/skimmed Crest of Stars, Banner of Stars I and started Banner of Stars II and I have to say, I'm not all that impressed with the production quality. I love the art, especially in the first two books, but the editing is not too impressive (with text placed awkwardly in the "bubbles") and the glossaries of Abh words seem to have been quite rushed as they are missing some terms that appear in the text (Though I haven't looked in the other books yet for terms I've encountered in one) and one of the definitions has been run into the previous, without the appropriate bolding and italicisation.

In short, I get the impression that these particular books didn't have very stringent proof-reading, etc before they went to press. Perhaps they were rushed out due to the US release of the anime?

If anyone knows what happened (my previous Tokyopop books have been pretty good), I'd be interested to know...

The Seikai Trilogy

The Seikai Trilogy

I made the mistake of going into Impact Comics on the way back to school today, and came out the owner of all three volumes of the Seikai Trilogy manga (redone in English by Tokyopop).

What I've seen of the anime (Crest of Stars, Banner of Stars and some of Banner of Stars II) that was based on the original novels is brilliant. It is fascinating watching the characters and their relationships grow and develop over the course of however many years.




Whilst in the shop, I noticed that they have most of Lone and Cub (forgive the lack of a link, but I can't find the Dark Horse site for the series anymore), which I'll have to finish off as I bought the first 19 volumes whilst I was in England a few years ago.

They also have a lot of stuff that just looks interesting. I can feel my fluid fiscal state evaporating as I think about it.