by J.N. Crossley, G.L. Mathai, and R.A.G. Seely
Abstract:
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 ]