We exploit a system of realizers for classical logic, and a translation from resolution into the sequent calculus, to assess the intuitionistic force of classical resolution for a fragment of intuitionistic logic. This approach is in contrast to formulating locally intuitionistically sound resolution rules. The techniques use the lambdamuepsilon-calculus, a development of Parigots lambdamu-calculus.
展开▼
