Abstract

The tableau substitution rule in free variable tableau reasoning is destructive, for in general, T has consequences that T0 lacks. We show how this destructive feature can be eliminated in favour of a set-up that replaces tableau substitution with the generation and incremental merge of variable constraints on tableau branches. The approach diifers from other constraint based techniques in tableau reasoning in that we constrain tableau branches rather than clauses, and use disunification constraints rather than unification constraints. We prove soundness and completeness, with the completeness proof based on a new way to generate models from open tableaux