We investigate the equational theory of Kleene algebra terms with variable complements -- (language) complement where it applies only to variables -- w.r.t. languages. While the equational theory w.r.t. languages coincides with the language equivalence (under the standard language valuation) for Kleene algebra terms, this coincidence is broken if we extend the terms with complements. In this paper, we prove the decidability of some fragments of the equational theory: the universality problem is coNP-complete, and the inequational theory t <= s is coNP-complete when t does not contain Kleene-star. To this end, we introduce words-to-letters valuations; they are sufficient valuations for the equational theory and ease us in investigating the equational theory w.r.t. languages. Additionally, we prove that for words with variable complements, the equational theory coincides with the word equivalence.

翻译：我们研究带有变量补的Kleene代数项（即补仅作用于变量的语言补）相对于语言的等式理论。对于Kleene代数项，相对于语言的等式理论在标准语言赋值下与语言等价性一致；然而，当我们在项中引入补后，这种一致性被打破。本文证明了该等式理论若干片段的可判定性：普遍性问题是coNP完全的，且当t不包含Kleene星时，不等式理论t ≤ s也是coNP完全的。为此，我们引入了“词到字母”赋值；这类赋值对于等式理论是充分的，并简化了相对于语言的等式理论的研究。此外，我们证明了对于带变量补的词，等式理论与词等價性一致。