关于逻辑装饰图变换的验证

我们处理带有诸如节点与边的\emph{添加}与\emph{删除}、节点\emph{合并}与\emph{克隆}、节点或边\emph{标记}以及边\emph{重定向}等动作的图变换的推理问题。首先，我们引入所考虑的图重写系统，其由给定逻辑 $\mathcal{L}$ 参数化。$\mathcal{L}$ 的公式用于标记图节点与边。第二步，我们利用类 Hoare 的最弱前置条件演算处理所考虑重写系统的形式验证问题。它作用于形如 $\{\texttt{Pre}\}(\texttt{R},\texttt{strategy}) \{\texttt{Post}\}$ 的三元组，其中 \texttt{Pre} 与 \texttt{Post} 是在给定逻辑 $\mathcal{L}$ 中规定的条件，\texttt{R} 是一个图重写系统，\texttt{strategy} 是说明 \texttt{R} 中规则如何被执行的表达式。我们证明所引入的演算是可靠的。此外，我们展示了所提框架如何能成功地用不同逻辑实例化。我们研究了一阶逻辑及其若干可判定片段，特别关注描述逻辑 (DL) 的不同方言。我们还通过互模拟关系表明，某些 DL 片段因其表达力不足而无法使用。