optimal, since it is shown that this logic is EXPTIME complete. We will study possible optimization (based for instance on caching techniques) in subsequent work.

## 5 Conclusion

In this paper, we have studied the logic CSL over minspaces, and we have obtained two main results: first we have provided a direct, sound and complete axiomatisation of this logic. Furthermore, we have defined a tableau calculus, which gives a decision procedure for this logic.

In [4], a tableau algorithm is proposed to handle logics for metric spaces comprising distance quantifiers of the form ∃ < a A and alike, where a is positive integer (together with an interior and a closure operator). As observed in [10], the operator ‡ can be defined in a related logic that allows quantification on the parameters in distance quantifiers. The methods proposed in [4] make use of an elegant relational translation to handle distance quantifiers with fixed parameters. However, it is not clear if they can be adapted to handle also the concept similarity operator.

There are a number of issues to explore in future research. The decision procedure outlined in the previous section is not guaranteed to have an optimal complexity, so that we can consider how to improve our calculus in order to match this upper bound. Another issue is the extension of our results to symmetric minspaces, and possibly to other classes of models. Finally, since one original motivation of CSL is to reason about concept similarity in ontologies, and particularly in description logics, we plan to study further its integration with significant languages of this family.

## References

1. George Boolos. The Logic of Provability. Cambridge University Press, 1993.

2. Laura Giordano, Valentina Gliozzi, Nicola Olivetti, and Camilla Schwind. Tableau calculi for preference-based conditional logics. In Marta Cialdea Mayer and Fiora Pirri, editors, TABLEAUX 2003, volume 2796 of Lecture Notes in Artificial Intelligence, pages 81-101. Springer, 2003.

3. Laura Giordano, Valentina Gliozzi, Nicola Olivetti, and Camilla Schwind. Tableau calculus for preference-based conditional logics : Pcl and its extensions. ACM
Transactions on Computational Logic (TOCL), to appear.

4. Ullrich Hustadt, Dmitry Tishkovsky, Frank Wolter, and Michael Zakharyaschev.

Automated reasoning about metric and topology. In JELIA'06, volume 4160 of L NAI, pages 490-493. Springer, 2006.

5. Agi Kurucz, Frank Wolter, and Michael Zakharyaschev.  Modal logics for metric spaces: Open problems. In Sergei N. Artemov, Howard Barringer, Artur S. d'Avila Garcez, Luís C. Lamb, and John Woods, editors, We Will Show Them! (2), pages 193-108. College Publications, 2005.

6. David Lewis. Counterfactuals. Basil Blackwell Ltd, 19 73.