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
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" }