On Testing Irreflexivity of Reduction Orderings for Combined Substitutions in Intuitionistic Matrix Proofs.
Daniel Korn, Christoph Kreitz.
In P. Baumgartner, R. Hähnle, J. Posegga, eds., 4th International Workshop on Theorem Proving with Analytic Tableaux and Related Methods (TABLEAUX'95) - Short Papers & Poster Sessions,, Universität Koblenz, Mai 1995, pp. 55-60.
Abstract
	In this paper we present a syntactical criterion for checking irreflexivity of the reduction ordering imposed by so-called combined substitutions which are part of the Matrix characterisation for first-order intuitionistic logic as presented by L. Wallen. The solution presented here is the concept of variable domains that can be considered as an extension of the well-known occurs-check technique.

		Paper is available in postscript and pdf format		A poster presented at the conference is available in compressed postscript and pdf format (Presentation: Daniel Korn)
Bibtex Entry					Back to overview of papers
	@InProceedings{inp:KornKreitz95a, author = "Daniel S.~Korn and Christoph Kreitz", title = "On Testing Irreflexivity of Reduction Orderings for Combined Substitutions in Intuitionistic Matrix Proofs", booktitle = "4$^{th}$ Workshop on Theorem Proving with Analytic Tableaux and Related Methods -- Short Papers \& Poster Sessions", year = 1995, editor = "P. Baumgartner and R. H{\"a}hnle and J. Posegga", pages = "55--60", publisher = "Universit{\"a}t Koblenz", address = "Institute of Computer Science" }