3
$\begingroup$

Is there any equational theory $T$ like $PV$ with following properties:

  1. 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)
  2. $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?

Thanks.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.