Is there any equational theory $T$ like $PV$ with following properties:
- If $T\vdash f=g$ for terms $f$ and $g$, translation of $f=g$ to propositional formulas has polynomial resolution proof.(like $PV$ and Extended resolution)
- $T$ proves soundness of resolution proof system.
I searched in the internet to find some papers answering above question, but I can not find anything. I found two papers about subsystems of $PV$ such that those subsystem have relation to weaker Frege proofs. Is there any reference answering this question?