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相同的计算复杂度。