First-Order Tableaux with Sorts

Tableau and the free variable tableau 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 $\gamma$ and $\delta$ rules. The standard unification algorithm of free variable tableau is replaced by a sorted unification algorithm. The resulting calculi, tableau with sorts and free variable tableau with sorts are proved sound, complete and more suitable for mechanization than their counterparts without sorts