A Constructively Adequate Refutation System for Intuitionistic Logic.
Daniel Korn, Christoph Kreitz.
In D. Galmiche, ed., 6th International Workshop on Theorem Proving with Analytic Tableaux and Related Methods (TABLEAUX'97) - Short Papers, Technical Report CRIN 97-R-030, Universite de Nancy II, 1997.
Abstract
	We present a refutation system for intuitionistic logic which allows to locate situations where constructive reasoning is unnecessary. In many subgoals of a derivation this property makes it possible to reduce the set of relevant reduction rules to a confluent one. As a result, backtracking over choicepoints for different orderings of non-permutable rules can often be avoided and the search space will be reduced considerably.

		Paper is available in postscript and pdf format		Slides of the conference presentation are available in compressed postscript and pdf format (Presentation: Daniel Korn)
Full version available as Technical Report AIDA-96-16 TU Darmstadt, FG Intellektik, November 1996.
Bibtex Entry					Back to overview of papers
	@InProceedings{inp:KornKreitz97a, author = "Daniel Korn and Christoph Kreitz", title = "A Constructively Adequate Refutation System for Intuitionistic Logic", booktitle = "6$^{th}$ Workshop on Theorem Proving with Analytic Tableaux and Related Methods -- Short Papers", year = 1997, editor = "D. Galmiche", series = "Technical Report CRIN 97-R-030" publisher = "Universit\'{e} de Nancy II" }