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.
No comments:
Post a Comment