用形式语法揭示时序逻辑模型的不可判定性，解决长期未解问题。
Analysing Temporal Reasoning in Description Logics Using Formal Grammars
- 通过时序逻辑与交集型文法的对应关系分析
- 证明查询回答在部分片段中不可判定
- 为新片段提供可判定性保证，复用现有算法
我们建立了（$\ ext{TEL}^\igcirc$）时序扩展描述逻辑与特定形式文法之间的对应关系，特别是带有交运算的合取文法（conjunctive grammars）。这一关联表明 $\ ext{TEL}^\igcirc$ 不具备模型的最终周期性，进一步导致其查询回答问题的不可判定性，解决了自 $\ ext{TEL}^\igcirc$ 提出以来悬而未决的关键问题。此外，该框架还使若干新的 $\ ext{TEL}^\igcirc$ 有趣片段的查询回答具有可判定性，并可复用现有的合取文法工具与算法。
原文摘要 · Abstract (English)
We establish a correspondence between (fragments of) $\mathcal{TEL}^\bigcirc$, a temporal extension of the $\mathcal{EL}$ description logic with the LTL operator $\bigcirc^k$, and some specific kinds of formal grammars, in particular, conjunctive grammars (context-free grammars equipped with the operation of intersection). This connection implies that $\mathcal{TEL}^\bigcirc$ does not possess the property of ultimate periodicity of models, and further leads to undecidability of query answering in $\mathcal{TEL}^\bigcirc$, closing a question left open since the introduction of $\mathcal{TEL}^\bigcirc$. Moreover, it also allows to establish decidability of query answering for some new interesting fragments of $\mathcal{TEL}^\bigcirc$, and to reuse for this purpose existing tools and algorithms for conjunctive grammars.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。