Abstract

In this article first-order semantic tableaux and free variable tableaux are extended with sorts. Sorts are sets of unary predicates. They can be attached to variables. Semantically, the domain of a variable is restricted to the intersection of the denotations of the attached predicates. Syntactically, the sort information is exploited by modified γ and δ tableaux rules. The standard unification algorithm of free variable tableaux is replaced by a sorted unification algorithm. The resulting calculi, tableaux with sorts and free variable tableaux with sorts are proved sound, complete and more suitable for mechanization than their standard counterparts without sorts