Terminating Tableaux for Graded Hybrid Logic with Global Modalities and Role Hierarchies
| Autor: | Gert Smolka, Mark Kaminski, Sigurd Schneider |
|---|---|
| Jazyk: | angličtina |
| Rok vydání: | 2010 |
| Předmět: |
FOS: Computer and information sciences
Blocking (linguistics) Normalization property Transitive relation Computer Science - Logic in Computer Science Theoretical computer science Modalities NEXPTIME General Computer Science Computer science Substructural logic Multimodal logic Intermediate logic Higher-order logic F.4.1 I.2.3 I.2.4 Logic in Computer Science (cs.LO) Theoretical Computer Science TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Description logic Chain (algebraic topology) Simple (abstract algebra) Dynamic logic (modal logic) Hybrid logic Mathematics |
| Zdroj: | Lecture Notes in Computer Science ISBN: 9783642027154 TABLEAUX |
| Popis: | We present a terminating tableau calculus for graded hybrid logic with global modalities, reflexivity, transitivity and role hierarchies. Termination of the system is achieved through pattern-based blocking. Previous approaches to related logics all rely on chain-based blocking. Besides being conceptually simple and suitable for efficient implementation, the pattern-based approach gives us a NExpTime complexity bound for the decision procedure. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|