Previous: AIDA-96-09 Next: AIDA-96-12 Index 1996

Intellectics Group: Technical Report 96-10

Efficiently Deciding Intuitionistic Propositional Logic via Translation into Classical Logic

Daniel Korn

In this paper we present a technique that translates propositional intuitionistic formulae into classical propositional formulae in an efficient way. 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 the existence of a finite countermodel for any intuitionistic non-theorem. This enables us to replace universal quantification over accessible worlds by a conjunction over the 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.

Full Paper: Compressed postscript Compressed DVI

BibTeX entry