Order Sorted Logic

12/13/09 under construction

Order Sorted Logic

Reading

[scan only]

A Oberschelp [1990] 'Order-Sorted Predicate Logic' in K.H.Blasius et al. eds.[1990] Sorts and Types in Artificial Intelligence

Tutorial

We have seen that sorted logic is more natural in most settings (for example, we don't want to be concerning ourselves with whether Julius Caesar is or is not a prime number).

And the sorts may well be disjoint: people are one sort, numbers are another sort, and nothing is both.

But actually it turns out that in many cases it is better for the sorts not to be disjoint. A good example is any classification system

classDiagram

Stratifying the universe here does not appropriate. If we want to have a sort for Fish, and another for Vertebrates, we do not want these to be disjoint simply because Fish are Vertebrates. Overlapping sorts are also common in mathematics; for example, mathematicians talk of the Natural Numbers, the Rational Numbers, the Real Numbers, the Complex Numbers, etc. but the Natural Numbers are part of the Rationals and the Rationals are included in the Reals and the Reals are included in the Complex. 

What is needed is a partial order on sorts. Sorts can be disjoint, but sometimes some sorts are subsorts of other sorts. The result is 'order sorted logic'.

Accommodating order sorted logic within our software systems

We actually already have it, at a rough and ready hand waving level suitable for an educational introduction.

Type labels parallel sorts, and type labels that can have subtypes and supertypes (eg s<t) parallel order sorted logic. Conceptually they are different, because with types there is only one universe or domain, and with sorts there are, or can be, several domains. But at the level of syntactical formulas and doing derivations, trees, etc, they can be treated as being the same.