Sciweavers

DLOG
2009
13 years 9 months ago
Terminating Tableaux for SOQ with Number Restrictions on Transitive Roles
Abstract. We show that the description logic SOQ with number restrictions on transitive roles is decidable by a terminating tableau calculus. The language decided by the calculus i...
Mark Kaminski, Gert Smolka
TABLEAUX
2009
Springer
14 years 6 months ago
Automated Synthesis of Tableau Calculi
This paper presents a method for synthesising sound and complete tableau calculi. Given a specification of the formal semantics of a logic, the method generates a set of tableau i...
Renate A. Schmidt, Dmitry Tishkovsky
TABLEAUX
2009
Springer
14 years 6 months ago
Terminating Tableaux for Graded Hybrid Logic with Global Modalities and Role Hierarchies
We present a terminating tableau calculus for graded hybrid logic with global modalities, reflexivity, transitivity and role hierarchies. Termination of the system is achieved thr...
Mark Kaminski, Sigurd Schneider, Gert Smolka
CADE
2008
Springer
15 years 4 days ago
Terminating Tableaux for Hybrid Logic with the Difference Modality and Converse
Abstract. We present the first terminating tableau calculus for basic hybrid logic with the difference modality and converse modalities. The language under consideration is basic m...
Mark Kaminski, Gert Smolka