Oxford Eprints
(1.101 recursos)
Oxford E-prints is a cross-disciplinary digital archive for research articles written by Oxford University authors. The repository has been developed as part of the SHERPA (Securing a Hybrid Environment for Research Preservation and Access) project and is running on eprints.org open archives software.
Mostrando recursos 1 - 1 de 1
1.
Proof-terms for classical and intuitionistic resolution - Ritter, E; Pym, D; Wallen, L
We extend Parigot's lambda mu 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, upsilon, 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...
(pdf ARRAY(0x1452dc20)) - 07-mar-2005
1.
