Many well-known logical identities are naturally written as equivalences between contextual formulas. A simple example is the Boole-Shannon expansion $c[p] \equiv (p \wedge c[\mathrm{true}] ) \vee (\neg\, p \wedge c[\mathrm{false}] )$, where $c$ denotes an arbitrary formula with possibly multiple occurrences of a "hole", called a context, and $c[\varphi]$ denotes the result of "filling" all holes of $c$ with the formula $\varphi$. Another example is the unfolding rule $\mu X. c[X] \equiv c[\mu X. c[X]]$ of the modal $\mu$-calculus. We consider the modal $\mu$-calculus as overarching temporal logic and, as usual, reduce the problem whether $\varphi_1 \equiv \varphi_2$ holds for contextual formulas $\varphi_1, \varphi_2$ to the problem whether $\varphi_1 \leftrightarrow \varphi_2$ is valid . We show that the problem whether a contextual formula of the $\mu$-calculus is valid for all contexts can be reduced to validity of ordinary formulas. Our first result constructs a canonical context such that a formula is valid for all contexts if{}f it is valid for this particular one. However, the ordinary formula is exponential in the nesting-depth of the context variables. In a second result we solve this problem, thus proving that validity of contextual formulas is EXP-complete, as for ordinary equivalences. We also prove that both results hold for CTL and LTL as well. We conclude the paper with some experimental results. In particular, we use our implementation to automatically prove the correctness of a set of six contextual equivalences of LTL recently introduced by Esparza et al. for the normalization of LTL formulas. While Esparza et al. need several pages of manual proof, our tool only needs milliseconds to do the job and to compute counterexamples for incorrect variants of the equivalences.

翻译：许多著名的逻辑恒等式自然地表示为上下文公式之间的等价关系。一个简单的例子是布尔-香农展开式 $c[p] \equiv (p \wedge c[\mathrm{true}] ) \vee (\neg\, p \wedge c[\mathrm{false}] )$，其中 $c$ 表示一个可能包含多个“洞”（称为上下文）的任意公式，而 $c[\varphi]$ 表示用公式 $\varphi$ “填充” $c$ 的所有洞的结果。另一个例子是模态 $\mu$-演算的展开规则 $\mu X. c[X] \equiv c[\mu X. c[X]]$。我们将模态 $\mu$-演算视为总领的时序逻辑，并像通常那样，将上下文公式 $\varphi_1, \varphi_2$ 是否满足 $\varphi_1 \equiv \varphi_2$ 的问题，归结为 $\varphi_1 \leftrightarrow \varphi_2$ 是否有效的问题。我们证明了，判断一个 $\mu$-演算的上下文公式是否对所有上下文都有效的问题，可以归约为普通公式的有效性问题。我们的第一个结果构造了一个典范上下文，使得一个公式对所有上下文有效当且仅当它对这个特定的上下文有效。然而，由此得到的普通公式的大小相对于上下文变量的嵌套深度是指数级的。在第二个结果中，我们解决了这个问题，从而证明了上下文公式的有效性问题与普通等价式一样，是 EXP-完全的。我们还证明了这两个结果对于 CTL 和 LTL 同样成立。我们在文末给出了一些实验结果。特别地，我们使用我们的实现来自动证明 Esparza 等人最近为 LTL 公式规范化而引入的一组六个 LTL 上下文等价式的正确性。虽然 Esparza 等人需要数页的手动证明，我们的工具仅需毫秒即可完成此工作，并为等价式的不正确变体计算出反例。