We present a technique that efficiently translates prepositional intuitionistic formulas into propositional classical formulas. This technique allows the use of arbitrary classical theorem provers for deciding the intuitionistic validity of a given propositional formula. The translation is based on the constructive description of a finite counter-model for any intuitionistic non-theorem. This enables us to replace universal quantification over all accessible worlds by a conjunction over the constructed finite set of these worlds within the encoding of a refuting Kripke-frame. This way, no additional theory handling by the theorem prover is required.
CITATION STYLE
Korn, D. S., & Kreitz, C. (1997). Deciding intuitionistic propositional logic via translation into classical logic. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1249, pp. 131–145). Springer Verlag. https://doi.org/10.1007/3-540-63104-6_15
Mendeley helps you to discover research relevant for your work.