Construct proof systems for common algorithmic task, like equivalence of regular expressions

Question

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?

Answer 1

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.

Answer 2

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.