Proof-terms for classical and intuitionistic resolution
Eike Ritter · Journal of Logic and Computation · 2000
We extend Parigot's λμ-calculus to form a system of realizers 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, υ, which realizes classical, multiple-conclusioned disjunction, and (ii) explicit substitutions, ∈, 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 characterization of the intuitionistic force 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 but, more significantly, they support a type-theoretic analysis of search spaces in both classical and intuitionistic logic.