Free Variable Tableaux for a Many Sorted Logic with Preorders

. We propose a sound and complete free variable semantic tableau method for handling many-sorted preorders in a first order logic, where functions and predicates behave monotonically or antimonotonically. We formulate additional expansion tableau rules as a more efficient alternative to adding the axioms characterizing a preordered structure. Completeness of the system is proved in detail. Examples and applications are introduced. 1 Introduction The use of non-symmetric relations and in particular inequalities, has become an interesting work line in several fields of computer science. For instance, ordered sorts in equational and object-oriented programming [GM 92], constraints in declarative programming languages [JM 94], nondeterministic specifications [Hus 91], among many others, all of them consider the use of preorders on expressions. In these cases, the logical framework is usually a generalization of the equational logic which includes a specific handling of preorders. Among t..