Tableau Methods for Modal and Temporal Logics in Handbook of Tableau Methods, M D'Agostino, D Gabbay, R Haehnle, J Posegga (Eds.), Kluwer Academic Publishers, 1999.
I've been reading Rajeev Goré's chapter on tableau methods for modal logics for the last few days. I think I'm starting to understand the unlabelled tableau systems now, though I still don't see why one would want to use an unlabelled tableau calculus over a labelled one, especially for mechanisation. This new-found semi-understanding makes me think that I'm going to have to re-read the Matsumoto and Mouri papers I looked at last week.
I've still not encountered anything about counter-model extraction in Goré yet, perhaps it was only meant to introduce me to the basics. I'm not yet sure, but since I've started reading these papers, I've developed a bit of a sinking feeling: perhaps counter-model extraction won't be as challenging as we expect. I'd really rather not have implementation issues of the user interface aspect dominating my thesis, if at all possible. Perhaps I'll be able to take a detour through one of the more unusual logics to demonstrate the counter-model extraction...
What ever happens, I've got a lot of work (and reading) ahead of me. I won't know if it'll all be worth it until I get my first class [finger crossed] Honours at the end of the year, but here's hoping.
Subscribe to:
Post Comments (Atom)
No comments:
Post a Comment