"Efficient Reasoning with Labelled Formula Translations of K"
Jens Happe, School of Computing Science, SFU
Thursday, May 20, 2004, 1:30 pm
Modal and Description Logics provide a solid, well-understood foundation for
Automated Reasoning. Systems have advanced to the point of being
successfully used in real-world applications such as medical reasoning and verification. However, with increasing problem size, the efficiency of
systems quickly deteriorates, as reasoning in ``interesting'' modal logics is intractable.
I propose a new framework to represent both modal formulas and their models in a more space-efficient way than is possible in traditional, Kripke-style models. I will argue why my representation will allow faster reasoning than is currently possible, even with today's highly optimized theorem provers.
This is a poster presentation which will be given at the KR 2004Doctoral Consortium at Whistler in June. Therefore, I wish to encourage suggestions, criticism and discussion from the audience. The presentation will be kept short, so there will be ample room for questions. A preprint of my poster will be displayed.