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?



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.