Previous: TR 94-11 Next: TR 94-17


Intellektik: Technical report 94-12

On Testing Irreflexivity of Reduction Orderings for Combined Substitutions in Intuitionistic Matrix Proofs

Daniel S. Korn and C. Kreitz

We are currently working on a stepwise transformation of Lincoln Wallen's matrix characterisation for validity of formulae in intuitionistic logic into a complete and correct connection procedure.

In this paper we focus on a syntactical criterion for checking irreflexivity of the reduction ordering imposed by so--called combined substitutions which are part of the characterisation.

The solution presented here is the concept of variable domains. Additionally we show that some of the constraints for the reduction ordering that arise when performing substitutions can be dropped without losing correctness.

Full Paper: Compressed postscript Compressed DVI

BibTeX entry