Some remarks on the possibility of extending resolution proof procedures to intuitionistic logic (Q1820590)

The author proposes a resolution procedure for propositional intuitionistic logic, which is indirect: the intuitionistic logic is translated into a modal system to which the rules of resolution are applied. The modal system used (it has the same Kripke interpretation as intuitionistic logic) is the S4 system of Lewis enriched by the axiom: ''p\(\to \square p\) if p is atomic''. The author defines the modal system, the translation rules, and the resolution rules. Also, a sketch of the completeness proof is presented. Unfortunately, as the author mentions, the backtrack to intuitionistic logic (possibly limited to this particular approach only) is extremely difficult since, among other things, a modal deduction formula from a set of clauses which translate intuitionistic formulas generates clauses which translate no intuitionistic formula.