Home  Online Resources  Table of Contents

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: exr@cs.bham.ac.uk, 2Department of Computer Science, Queen Mary and Westfield College, University of London, Mile End Road, London E1 4NS, UK, E-mail: pym@dcs.qmw.ac.uk, 3Oxford University Computing Laboratory, Wolfson Building, Parks Road, Oxford, OX1 3QD, UK, E-mail: lw@comlab.ox.ac.uk

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.

  Full-Text PDF  (317 KB)


[ Oxford University Press]   [ Oxford Journals]   [ Comments & Feedback]   Copyright© Oxford University Press, 2000.