# Lógica polissortida

A lógica polissortida pode refletir formalmente a nossa intenção de não lidar com o universo como um conjunto homogêneo de objetos, mas particionar isso de uma maneira que é semelhante aos de tipos em linguagens tipadas. Ambos funcionais e assertivas "partes do discurso" na linguagem da logica refletem essa partição tipificada do universo, mesmo no nível de sintaxe: substituição e argumento de passagem só pode ser feito em conformidade, respeitando os "tipos".
Há mais maneiras de formalizar a intenção acima mencionada; a Lógica polissortida é qualquer pacote de informação que o preenche. Na maioria dos casos, são os seguintes dados:
* um conjunto de tipos, S
* uma generalização adequada da noção de assinatura ara ser capaz de lidar com a informação adicional que vem com os tipos.
O universo de discurso de qualquer estrutura dessa assinatura é então fragmentada em subconjuntos dijuntos, um para cada tipo.

## Exemplo

Ao refletirmos sobre criaturas biológicas, é útil distinguir dois tipos: ${\textit {plant}}$ and ${\textit {animal}}$. Enquanto uma função ${\textit {mother}}:{\textit {animal}}\longrightarrow {\textit {animal}}$ faz sentido, uma função similar ${\textit {mother}}:{\textit {plant}}\longrightarrow {\textit {plant}}$ usualmente não faz não faz. Lógica polissortida permite um ter termos como ${\textit {mother}}({\textit {lassie}})$, mas discartar termos como ${\textit {mother}}({\textit {my\_favorite\_oak}})$ como sintaticamente mal formado.

## Álgebra

A álgebra da lógica polissortida é explicada em um artigo de Caleiro e Gonçalves, que generaliza a lógica algébrica abstrata para o caso polissortido, mas também pode ser usado como material introdutório.

## Lógica ordem-sortida

Enquanto Lógica polissortida requer dois diferentes tipos para ter conjuntos universo dijuntos, lógica ordem-sortida permite um tipo $s_{1}$ para ser declarado como um subtipo de outro tipo. $s_{2}$, usualmente escrevendo$s_{1}\subseteq s_{2}$ ou sintaxe similar. No exemplo abaixo, é desejável declarar
    ${\textit {dog}}\subseteq {\textit {carnivore}}$,
    ${\textit {dog}}\subseteq {\textit {mammal}}$,
    ${\textit {carnivore}}\subseteq {\textit {animal}}$,
    ${\textit {mammal}}\subseteq {\textit {animal}}$,
    ${\textit {animal}}\subseteq {\textit {creature}}$,
    ${\textit {plant}}\subseteq {\textit {creature}}$,
e assim por diante.
Onde um termo de um tipo $s$ é requerido, um termo de qualquer subtipo $s$ pode ser fornecido em seu lugar. Por exemplo, assumindo uma declaração de função ${\textit {mother}}:{\textit {animal}}\longrightarrow {\textit {animal}}$, e uma declaração constante ${\textit {lassie}}:{\textit {dog}}$, o termo ${\textit {mother}}({\textit {lassie}})$ é perfeitamente válido e tem o tipo ${\textit {animal}}$. A fim de fornecer as informações de que a mãe de um cão é um cão, por sua vez, uma nova declaração ${\textit {mother}}:{\textit {dog}}\longrightarrow {\textit {dog}}$pode ser emitida; isso é chamado de sobrecarga de funções , semelhante ao Polimorfismo em linguagens de programação.
Lógica ordem-sortida pode ser traduzida em lógica não sortida, usando um predicado unário $p_{i}(x)$ para cada tipo$s_{i}$, e um axioma $\forall x:p_{i}(x)\rightarrow p_{j}(x)$ para cada declaração de subtipo $s_{i}\subseteq s_{j}$. A abordagem inversa foi bem sucedido na prova de teoremas automatizado: em 1985, Christoph Walther poderia resolver um problema, então referência, traduzindo-a na lógica ordem-sortida, portando fazendo isso uma ordem de magnitude, assim como muitos predicados unários se transformaram em tipos.
A fim de incorporar uma lógica classificados ordem em um teorema automatizado prover baseada em cláusulas, uma correspondente algoritmo de unificação ordem-sortida é necessário,que exige que para quaisquer dois tipos declarados $s_{1},s_{2}$ their intersection $s_{1}\cap s_{2}$ ser declarados, para: se $x_{1}$ e $x_{2}$ é im tipo variável $s_{1}$ e $s_{2}$, respectivamente, a equação $x_{1}{\stackrel {?}{=}}x_{2}$ possui a solução $\{x_{1}=x,\;x_{2}=x\}$, onde $x:s_{1}\cap s_{2}$.
Smolka generalizou a lógica ordem-sortida para permitir polimorfismo paramétrico.
IEm seu quadro, declarações de subtipo são propagadas para expressões do tipo complexo. Como um exemplo de programação, um tipo paramétrico ${\textit {list}}(X)$ pode ser declarado (with $X$ sendo um tipo paramétrico como em um template C++), e de uma declaração de subtipo ${\textit {int}}\subseteq {\textit {float}}$ a relação ${\textit {list}}({\textit {int}})\subseteq {\textit {list}}({\textit {float}})$ é automaticamente inferida, significando que cada lista de inteiros é também uma lista de tipos float.
Schmidt-Schauß generalizou ordem-sortida para permitir a declaração de termos. Como um exemplo, asumindo declarações de subtipos ${\textit {even}}\subseteq {\textit {int}}$ e ${\textit {odd}}\subseteq {\textit {int}}$, uma declaração de termo como $\forall i:{\textit {int}}.\;(i+i):{\textit {even}}$ permite declarar uma propriedade de adição de inteiros que não pode ser expressada por poliformismo ordinário.