Terminating Tableaux for $\mathcal{SOQ}$ with Number Restrictions on Transitive Roles

Abstract : We show that the description logic $\mathcal{SOQ}$ with number restrictions on transitive roles is decidable by a terminating tableau calculus. The language decided by the calculus includes the universal role, which allows us to internalize TBox axioms. Termination of the system is achieved through pattern-based blocking.
Type de document :
Communication dans un congrès
Cristian S. Calude; Vladimiro Sassone. 6th IFIP TC 1/WG 2.2 International Conference on Theoretical Computer Science (TCS) / Held as Part of World Computer Congress (WCC), Sep 2010, Brisbane, Australia. Springer, IFIP Advances in Information and Communication Technology, AICT-323, pp.213-228, 2010, Theoretical Computer Science. 〈10.1007/978-3-642-15240-5_16〉
Liste complète des métadonnées

Littérature citée [24 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01054458
Contributeur : Hal Ifip <>
Soumis le : mercredi 6 août 2014 - 16:25:36
Dernière modification le : mardi 31 octobre 2017 - 14:22:11
Document(s) archivé(s) le : mercredi 26 novembre 2014 - 01:00:49

Fichier

03230214.pdf
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Citation

Mark Kaminski, Gert Smolka. Terminating Tableaux for $\mathcal{SOQ}$ with Number Restrictions on Transitive Roles. Cristian S. Calude; Vladimiro Sassone. 6th IFIP TC 1/WG 2.2 International Conference on Theoretical Computer Science (TCS) / Held as Part of World Computer Congress (WCC), Sep 2010, Brisbane, Australia. Springer, IFIP Advances in Information and Communication Technology, AICT-323, pp.213-228, 2010, Theoretical Computer Science. 〈10.1007/978-3-642-15240-5_16〉. 〈hal-01054458〉

Partager

Métriques

Consultations de la notice

147

Téléchargements de fichiers

64