Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadata

Cited literature [24 references]  Display  Hide  Download

https://hal.inria.fr/hal-01054458
Contributor : Hal Ifip <>
Submitted on : Wednesday, August 6, 2014 - 4:25:36 PM
Last modification on : Tuesday, October 31, 2017 - 2:22:11 PM
Long-term archiving on: : Wednesday, November 26, 2014 - 1:00:49 AM

File

03230214.pdf
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

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⟩

Share

Metrics

Record views

271

Files downloads

221