A more expressive formulation of many sorted logic

Many sorted logics can increase deductive efficiency by eliminating useless branches of the search space, but usually this results in reduced expressiveness. The many sorted logic described here has several unusual features which not only increase expressiveness but also can reduce the search space even more than a conventional many sorted logic. The quantifiers are unsorted: the restriction on the range of a variable derives from the argument positions of the nonlogical symbols that it occupies. Polymorphic sort specifications are allowed; thus statements usually requiring several assertions may be compactly expressed by a single assertion. The sort structure may be an arbitrary lattice and the sort of a term can be more general than the sort of the argument position it occupies. It is also shown how it is sometimes possible to use sort information to determine the truth value of a formula without resort normal inference. Inference rules for a resolution based system are discussed; these can be proved to be sound and complete.