by J.N. Crossley, G.L. Mathai, and R.A.G. Seely
A logical calculus, not unlike Gentzen's sequent calculus for intuitionistic logic, is described which is sound for polynomial-time realizability as defined by Crossley and Remmel. The sequent calculus admits cut-elimination, thus giving a decision procedure for the propositional fragment.
[ This paper has appeared in Methods of Logic in Computer Science, Vol 1, No 3 (1994) pp 279 - 298 ]