Lecture
Many-sorted logic can formally reflect our intention not to treat the universe as a homogeneous collection of objects, but to partition it in a way analogous to types in typed programming . Both the functional and the predicative « parts of speech » in the language of logic reflect this typed partitioning of the universe, even at the syntactic level: substitution and the passing of arguments can be carried out only in the corresponding way, taking «sorts» into account.
There are various ways of formalizing the above-mentioned intention; many-sorted logic is any package of information that implements it. In most cases, the following are provided:
The domain of discourse of any structure of this signature is then fragmented into disjoint subsets, one for each sort.
When reasoning about biological organisms, it is useful to distinguish two sorts 
and 
. While the function 
makes sense, a similar function 
usually does not. Many-sorted logic allows terms such as 
, but rejects terms of the form 
as syntactically ill-formed.
The algebraization of many-sorted logic is explained in the paper by Caleiro and Gonçalves , which generalizes abstract algebraic logic to the many-sorted case, but can also be used as introductory material.
Example of a sort hierarchy
While many-sorted logic requires two distinct sorts in order to have disjoint universe sets, order-sorted logic allows one sorts1
to be declared a subsort of another sort 
, usually by writing 
or similar syntax. In the biology example above, it is desirable to declare
dog⊆carnivore 
,
dog⊆mammal 
,
carnivore⊆animal 
,
mammal⊆animal 
,
animal⊆organism
,
plant⊆organism
,
etc.; see figure.
Wherever a term of sorts
is required, a term of any subsort ofscan be used instead. This is the Liskov substitution principle . For example, if a function is declared 
, and a constant is declared 
, the term )
is perfectly valid and has sort 
To provide the information that the mother of a dog is, in turn, also a dog, one more declaration must be made. 
can be issued; this is called function overloading , analogous to overloading in programming languages .
Order-sorted logic can be translated into unsorted logic by using a unary predicatep 
for each sorts
, and an axiom 
for each subsort declaration 
The converse approach has proved successful in automated theorem proving: in 1985 Christoph Walther was able to solve the then-benchmark problem by translating it into order-sorted logic, thereby reducing it by an order of magnitude, since many unary predicates turned into sorts.
To incorporate order-sorted logic into a clause-based automated theorem prover, a corresponding algorithm for order-sorted unification is needed, which requires that for any two declared sorts 
their intersection 
must also be declared: if 
and 
are variables of sort and , respectively, the equation 
has the solution 
, where 
.
Smolka generalized order-sorted logic to provide parametric polymorphism . In his framework, subsort declarations extend to expressions of complex types. As a programming example, one can cite a parametric sort 
can be declared (with 
being a type parameter, as in a C++ template ), and from the subsort declaration 
the relation 
is automatically derived, meaning every list of integers is also a list of floating-point numbers.
Schmidt-Schauß generalized order-sorted logic to allow term declarations. For example, suppose the subsort declarations 
and 
, a term declaration such as 
allows declaring a property of integer addition that cannot be expressed by ordinary overloading.
Comments