<p>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)$.</p>

<p>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.</p>

CC BY-SA 3.0
2017-04-18T08:27:39.507Z
As far as I understand it, the algorithm is *not* polynomial-time.
Emil Jeřábek
CC BY-SA 3.0
2017-04-18T09:37:07.837Z
Could you please be more specific what would be coded into the string representing the proof to make it polynomial-time checkable?
StefanH
CC BY-SA 3.0
2017-04-18T12:42:28.403Z
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.
Kaveh
CC BY-SA 3.0
2017-04-18T04:01:18.220Z
2017-04-19T03:32:17.833Z
2017-04-19T03:32:17.833Z
Kaveh
<p>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:</p>

<p><a href="http://anupamdas.com/items/hka/hka.pdf" rel="nofollow noreferrer">A cut-free cyclic proof system for Kleene Algebra</a></p>

<p>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.</p>

CC BY-SA 3.0
2017-05-05T13:23:14.390Z
2017-05-05T13:23:14.390Z
Anupam Das
<p>A <a href="https://en.wikipedia.org/wiki/Propositional_proof_system" rel="nofollow noreferrer">propositional proof system</a> 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.</p>

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

<p>Here is a <a href="https://cstheory.stackexchange.com/questions/14088/intuition-behind-proof-systems">post on the intuition</a>, but I do not get it when I want to apply it.</p>

<p>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. </p>

<p>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. </p>

<p>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?).</p>

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

CC BY-SA 3.0
2017-04-18T06:32:04.037Z
Equivalence of regular expressions is PSPACE-complete, so you shouldn't expect to have short propositional encodings.
Sylvain
CC BY-SA 3.0
2017-04-18T08:33:55.353Z
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.
Emil Jeřábek
<lo.logic><fl.formal-languages><proof-complexity><descriptive-complexity>
Construct proof systems for common algorithmic task, like equivalence of regular expressions
StefanH
# Construct proof systems for common algorithmic task, like equivalence of regular expressions

(Asked by: username_0 on 2017-04-17)

A [propositional proof system](https://en.wikipedia.org/wiki/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](https://cstheory.stackexchange.com/questions/14088/intuition-behind-proof-systems), 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?

**Tags:** lo.logic, fl.formal-languages, proof-complexity, descriptive-complexity

> **Comments:**
> **username_1**: Equivalence of regular expressions is PSPACE-complete, so you shouldn't expect to have short propositional encodings.  
> **username_2**: 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.  

---

## 2 answers

### Answer by username_3 on 2017-04-18. Score: 3

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.

> **Comments:**
> **username_2**: As far as I understand it, the algorithm is *not* polynomial-time.  
> **username_0**: Could you please be more specific what would be coded into the string representing the proof to make it polynomial-time checkable?  
> **username_3**: 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.  

---

### Answer by username_4 on 2017-05-05. Score: 2

username_3'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](http://anupamdas.com/items/hka/hka.pdf)

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.


---

