Satisfiability is the fundamental NP-complete problem. Cook-Reckhow theorem states that the existence of a propositional proof system that admits polynomial size proofs for all tautologies implies that NP=coNP. In principle, every NP-complete problem can encode Satisfiability problem. It seems to me that we should be able systematically generate a proof system from any NP-complete problem. The aim is that this may give new insights into proving proof complexity lower bounds. I am looking for references.