Item

Abstract

This paper provides two results concerning Order-Sorted Logic with Term
Declarations. First, we show that linear term declarations can be transformed
conservatively into function declarations, thus yielding elementary signatures.
This provides a simple proof of the well known fact that unification in linear
signatures is decidable. A similar transformation exists for semi-linear term
declarations, resulting in shallow term declarations. Secondly, we provide an
inference system transforming sort constraints over an arbitrary signature into
almost solved form. The step from almost solved forms to solved forms requires
a procedure to decide emptiness of sort intersections, which is not possible in
general. This shows that it is the sort intersection problem that accounts for
the undecidability of unification in signatures with term declarations.