A propositional proof system according to Cook and Reckhow for a language $L \subseteq \Sigma^{\ast}$ is a deterministic polynomial time function $f : \Sigma^{\ast} \to L$ that is onto.

For $y \in L$ a word $x \in \Sigma^{\ast}$ with $f(x) = y$ is called a proof for $y$.

Here is a post on the intuition, but I do not get it when I want to apply it.

For example, if I consider the language $$ EQUIV = \{ (u,v) : \mbox{$u$ and $v$ are equivalent regular expressions} \} $$ then I know an algorithm for this language would be to convert these regular expression into NFA's, determinize them and minimize them and then check if they are isomorphic.

But how would a proof system for $EQUIV$ look like? Would it be a surjective function $f : \Sigma^{\ast} \to EQUIV$ where the arguments somehow codes the regular expression, DFA's for them and an isomorphism between those DFA's? Then $f$ would simply check if the isomorphism is a valid isomorphism between the DFA's, guess this would be a simple task.

But how to check that the regular expression belong to the DFA's, I am not sure if that would be an easy task as it involves computing DFA's for regular expressions, which might take exponential time, or? Or could it code additional DFA's which could easily be composed to REGEXPs with some fixed algorithms (but is it then easy to check that these give isomorphic minimal DFA's as the given ones? I mean that includes to find an isomorphism, which is not easy, so code that again into the input?).

Or am I on the wrong track, might a proof system look totally different?

  • $\begingroup$ Equivalence of regular expressions is PSPACE-complete, so you shouldn't expect to have short propositional encodings. $\endgroup$
    – Sylvain
    Apr 18, 2017 at 6:32
  • $\begingroup$ You can afford time polynomial in the size of the "proof", not just the original input. Construction of a DFA takes exponential time because the DFA may have exponential size, but if you already have it, you can verify it in time polynomial in the size of the DFA + the size of the regular expression. $\endgroup$ Apr 18, 2017 at 8:33

2 Answers 2


You have a non-deterministic algorithm deciding the problem. If you want to think of it as a proof system for $EQUIV$, then the proof of $(u,v) \in EQUIVE$ is just the string representing the computation of your algorithm on $(u,v)$. The proof checker just checks that the given string is in fact an accepting computation of your algorithm on $(u,v)$.

Use the alternative definition of proof system, it is often easier to think about: an algorithm that gets a formula and a string and checks if the string of a proof of the formula, rather than a function that checks if a given string of is proof and if so outputs the proven formula.

  • $\begingroup$ As far as I understand it, the algorithm is not polynomial-time. $\endgroup$ Apr 18, 2017 at 8:27
  • $\begingroup$ Could you please be more specific what would be coded into the string representing the proof to make it polynomial-time checkable? $\endgroup$
    – StefanH
    Apr 18, 2017 at 9:37
  • $\begingroup$ computation is the encoded list of machine configurations. see e.g. the proof put NP-completeness of SAT where we encode the computations of arbitrary polynomial time NTMs. $\endgroup$
    – Kaveh
    Apr 18, 2017 at 12:42

Kaveh's response exemplifies well the Cook-Reckhow notion of an abstract proof system. Nonetheless, for comparison, I point to a recent preprint of mine and Damien Pous:

A cut-free cyclic proof system for Kleene Algebra

Here we give a more traditional bona fide proof system for equivalence of regular expressions by allowing non-wellfounded reasoning in proofs. Soundness is ensured by a global criterion that is polynomial-time checkable, so indeed it is a proof system in the Cook-Reckhow sense.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.