Monotonic preorders are integrated into tableaux using a simultaneous rigid unification calculus. For the case where monotonicity is not considered, a sound, complete and terminating calculus is defined and subsequently refined by using rewrite techniques. For the monotonic case, a sound and existentially complete calculus is presented which avoids the computation of some naive solutions.

You do not currently have access to this article.