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
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.