A Constructively Adequate Refutation System for Intuitionistic Logic.
Daniel Korn, Christoph Kreitz.
Technical Report AIDA-96-16, TU Darmstadt, FG Intellektik, November 1996.
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.

			Back to overview of papers
Bibtex Entry
	@TechReport{tr:KornKreitz96a, author = "Daniel Korn and Christoph Kreitz", title = "A Constructively Adequate Refutation System for Intuitionistic Logic", institution = "FG Intellektik, TU Darmstadt", year = "1996", number = "AIDA--96--16", month = "November" }