Abstract
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 λμε-calculus, a development of Parigot's λμ-calculus.
Cite
CITATION STYLE
Ritter, E., Pym, D., & Wallen, L. (1996). Proof-terms for classical and intuitionistic resolution. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1104, pp. 17–31). Springer Verlag. https://doi.org/10.1007/3-540-61511-3_66
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
