Journal of Logic and Computation, Volume 10, Issue 2, pp. 173-207: Abstract.
Proof-terms for classical and intuitionistic resolution
E Ritter1, D Pym2 and L Wallen3
1School of Computer Science, University of Birmingham, Edgbaston, Birmingham B15 2TT, UK, E-mail: firstname.lastname@example.org, 2Department of Computer Science, Queen Mary and Westfield College, University of London, Mile End Road, London E1 4NS, UK, E-mail: email@example.com, 3Oxford University Computing Laboratory, Wolfson Building, Parks Road, Oxford, OX1 3QD, UK, E-mail: firstname.lastname@example.org
We extend Parigot's [lgr][mgr]-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, [ugr], which realizes classical, multiple-conclusioned disjunction, and (ii) explicit substitutions, [isin], 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.
Keywords: proof-search, theorem proving, resolution, classical logic, intuitionistic logic, [lgr]-calculus.