CSL-lean: A theorem-Prover for the logic of Comparative Concept Similarity

The logic CSL of the comparative concept similarity has been introduced by Sheremet, Tishkovsky, Wolter and Zakharyaschev to capture a form of qualitative similarity comparison between concepts and/or objects. In this logic we can formulate assertions of the form “objects A are more similar to B than to C”. This kind of assertions can be added to an ontology to express qualitative comparisons between concepts. In this work we present CSL-lean, the first theorem-prover for this logic. It is a direct Prolog implementation of a tableaux-based decision procedure recently proposed for this logic. The Prolog program is inspired by the lean-methodology.