We consider (logical) reasoning for regular expressions with lookahead (REwLA). In this paper, we give an axiomatic characterization for both the (match-)language equivalence and the largest substitution-closed equivalence that is sound for the (match-)language equivalence. To achieve this, we introduce a variant of propositional dynamic logic (PDL) on finite linear orders, extended with two operators: the restriction to the identity relation and the restriction to its complement. Our main contribution is a sound and complete Hilbert-style finite axiomatization for the logic, which captures the equivalences of REwLA. Using the extended operators, the completeness is established via a reduction into an identity-free variant of PDL on finite strict linear orders. Moreover, the extended PDL has the same computational complexity as REwLA.

翻译：本文研究带前瞻正则表达式（REwLA）的（逻辑）推理。我们为（匹配）语言等价性以及对于（匹配）语言等价性可靠的最大替换封闭等价关系给出了公理化刻画。为此，我们引入一种在有限线性序上的命题动态逻辑（PDL）变体，该逻辑扩展了两个算子：对恒等关系的限制算子及其补关系的限制算子。我们的主要贡献是为该逻辑提供了一个可靠且完备的希尔伯特式有限公理化系统，该系统刻画了REwLA的等价关系。借助扩展算子，通过归约到有限严格线性序上无恒等关系的PDL变体来建立完备性。此外，扩展PDL具有与REwLA相同的计算复杂度。