A Logical Calculus for Polynomial-Time Realizability

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 ]