Terminating Tableaux for $\mathcal{SOQ}$ with Number Restrictions on Transitive Roles - Theoretical Computer Science
Conference Papers Year : 2010

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.

Domains

Digital Libraries [cs.DL]
Fichier principal
Vignette du fichier
03230214.pdf (195.48 Ko) Télécharger le fichier
Origin Files produced by the author(s)

Hal Ifip  : Connect in order to contact the contributor

https://inria.hal.science/hal-01054458

Submitted on : Wednesday, August 6, 2014-4:25:36 PM

Last modification on : Thursday, December 5, 2024-2:12:05 PM

Long-term archiving on : Wednesday, November 26, 2014-1:00:49 AM

Download

Dates and versions

hal-01054458 , version 1 (06-08-2014)

Licence

Attribution

Identifiers

Cite

Mark Kaminski, Gert Smolka. Terminating Tableaux for $\mathcal{SOQ}$ with Number Restrictions on Transitive Roles. 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. pp.213-228, ⟨10.1007/978-3-642-15240-5_16⟩. ⟨hal-01054458⟩

Export

BibTeX XML-TEI Dublin Core DC Terms EndNote DataCite

Collections

IFIP IFIP-AICT IFIP-AICT-323 IFIP-TC IFIP-TC1 IFIP-TC2 IFIP-TCS IFIP-WG2-2 IFIP-WCC
118 View
93 Download

Altmetric

Share

More