On Regular Expression Proof Complexity of Salomaa’s Axiom System \(F_1\)

We investigate the proof complexity of Salomaa’s axiom system  \(F_1\) for regular expression equivalence. We show that for two regular expression E and F over the alphabet  \(\varSigma \) with \(L(E)=L(F)\) an equivalence proof of length at most \(O\left( |\varSigma |^4\cdot \textsc {Tower}(\max \{h(E),h(F)\}+4)\right) \) can be derived within  \(F_1\) , where h(E) (h(F), respectively) refers to the height of E (F, respectively) and the tower function is defined as \(\textsc {Tower}(1)=2\) and \(\textsc {Tower}(k+1)=2^{\textsc {Tower}(k)}\) , for  \(k\ge 1\) . In other words It is well known that regular expression equivalence admits exponential proof length if not restricted to the axiom system  \(F_1\) . From the theoretical point of view the exponential proof length seems to be best possible, because we show that regular expression equivalence admits a polynomial bounded proof if and only if \({\textsf{NP}}={\textsf{PSPACE}}\) .