A CUT-ELIMINATION PROCEDURE DESIGNED FOR EVALUATING PROOFS AS PROGRAMS

This paper describes a method which can be used to determine output values from given input values of programs taking the form of formal proofs. The proofs are constructed in a logic calculus which may include user-defined non-logical inference rules. This calculus is complete in the sense that each computable function can be computed by means of a proof in this calculus. The evaluation method is based mainly on Gentzen's cut-elimination procedure. However the presence of non-logical inference rules requires additional steps to eliminate these rules. Termination of the method is proved by assigning constructive ordinal numbers.