%0 Conference Proceedings
%T Terminating Tableaux for $\mathcal{SOQ}$ with Number Restrictions on Transitive Roles
%+ Saarland University [Saarbrücken]
%A Kaminski, Mark
%A Smolka, Gert
%< avec comité de lecture
%( IFIP Advances in Information and Communication Technology
%B 6th IFIP TC 1/WG 2.2 International Conference on Theoretical Computer Science (TCS) / Held as Part of World Computer Congress (WCC)
%C Brisbane, Australia
%Y Cristian S. Calude; Vladimiro Sassone
%I Springer
%3 Theoretical Computer Science
%V AICT-323
%P 213-228
%8 2010-09-20
%D 2010
%R 10.1007/978-3-642-15240-5_16
%Z Computer Science [cs]/Digital Libraries [cs.DL]Conference papers
%X 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.
%G English
%2 https://inria.hal.science/hal-01054458/document
%2 https://inria.hal.science/hal-01054458/file/03230214.pdf
%L hal-01054458
%U https://inria.hal.science/hal-01054458
%~ IFIP
%~ IFIP-AICT
%~ IFIP-AICT-323
%~ IFIP-TC
%~ IFIP-TC1
%~ IFIP-TC2
%~ IFIP-TCS
%~ IFIP-WG2-2
%~ IFIP-WCC
%~ IFIP-2010