Many sorted logic

Example

When reasoning about biological creatures, it is useful to distinguish two sorts: plant and animal . While a function mother : animal ⟶ animal makes sense, a similar function mother : plant ⟶ plant usually does not. Many-sorted logic allows one to have terms like mother ( lassie ) , but to discard terms like mother ( my\_favorite\_oak ) as syntactically ill-formed.

Algebraization

The algebraization of many-sorted logic is explained in an article by Caleiro and Gonçalves, which generalizes abstract algebraic logic to the many-sorted case, but can also be used as introductory material.

Order-sorted logic

While many-sorted logic requires two distinct sorts to have disjoint universe sets, order-sorted logic allows one sort s 1 to be declared a subsort of another sort s 2 , usually by writing s 1 ⊆ s 2 or similar syntax. In the above example, it is desirable to declare

and so on.

Wherever a term of some sort s is required, a term of any subsort of s may be supplied instead. For example, assuming a function declaration mother : animal ⟶ animal , and a constant declaration lassie : dog , the term mother ( lassie ) is perfectly valid and has the sort animal . In order to supply the information that the mother of a dog is a dog in turn, another declaration mother : dog ⟶ dog may be issued; this is called function overloading, similar to overloading in programming languages.

Order-sorted logic can be translated into unsorted logic, using a unary predicate p i ( x ) for each sort s i , and an axiom ∀ x : p i ( x ) → p j ( x ) for each subsort declaration s i ⊆ s j . The reverse approach was successful in automated theorem proving: in 1985, Christoph Walther could solve a then benchmark problem by translating it into order-sorted logic, thereby boiling it down an order of magnitude, as many unary predicates turned into sorts.

In order to incorporate order-sorted logic into a clause-based automated theorem prover, a corresponding order-sorted unification algorithm is necessary, which requires for any two declared sorts s 1 , s 2 their intersection s 1 ∩ s 2 to be declared, too: if x 1 and x 2 is a variable of sort s 1 and s 2 , respectively, the equation x 1 = ? x 2 has the solution { x 1 = x , x 2 = x } , where x : s 1 ∩ s 2 .

Smolka generalized order-sorted logic to allow for parametric polymorphism. In his framework, subsort declarations are propagated to complex type expressions. As a programming example, a parametric sort list ( X ) may be declared (with X being a type parameter as in a C++ template), and from a subsort declaration int ⊆ float the relation list ( int ) ⊆ list ( float ) is automatically inferred, meaning that each list of integers is also a list of floats.

Schmidt-Schauß generalized order-sorted logic to allow for term declarations. As an example, assuming subsort declarations even ⊆ int and odd ⊆ int , a term declaration like ∀ i : int . ( i + i ) : even allows to declare a property of integer addition that could not be expressed by ordinary overloading.