Deciding Intuitionistic Propositional Logic via Translation into Classical Logic

Abstract. We present a technique that efficiently translates propositional 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 countermodel 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.

• Type: Conference
• Year: 1997
• Where: CADE
• Authors: Daniel S. Korn, Christoph Kreitz
• Keywords: CADE 1997, Intuitionistic, Logical Reasoning, Propositional Classical Formulas, Propositional Intuitionistic Formulas