Proof-terms for classical and intuitionistic resolution

We extend Parigot's lambda mu-calculus to form a system of reallsers for classical logic which reflects the structure of Gentzen's cut-free, multiple-conclusioned, sequent calculus LK when used as a system for proof-search. Specifically, we add (i) a second binding operator, nu, which realizes classical, multiple-conclusioned disjunction, and (ii) explicit substitutions epsilon, which provide sufficient term-structure to interpret the left rules of LK, A necessary and sufficient condition is formulated on realizers to characterize when a given (classical) realizer for a sequent witnesses the intuitionistic provability of that sequent, A translation between the classical sequent calculus and classical resolution due to Mints is used to lift the conditions to classical resolution, thereby giving a characterizatian of the intuitionistic farce of classical resolution. One application of these results is to allow standard resolution methods of uniform proof-search to be used directly for Intuitionistic logic bet, more significantly, they support a type-theoretic analysis of search spaces In both classical and intuitionistic logic.