Deciding Intuitionistic Propositional Logic via Translation into Classical Logic.
Daniel Korn, Christoph Kreitz.
In W. McCune, ed., 14th International Conference on Automated Deduction (CADE-14), LNAI 1249, pp. 131-145, Springer Verlag, 1997.
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.

		Paper is available in postscript and pdf format		Slides of the conference presentation are available in compressed postscript and pdf format (Presentation: Daniel Korn)
Bibtex Entry					Back to overview of papers
	@InProceedings{inp:KornKreitz97a, author = "Daniel Korn and Christoph Kreitz", title = "Deciding Intuitionistic Propositional Logic via Translation into Classical Logic", booktitle = "14$^{th}$ International Conference on Automated Deduction", year = 1997, editor = "W. McCune", volume = 1249, series = "Lecture Notes in Artificial Intelligence", pages = "131--145", publisher = "Springer Verlag" }