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: $\mathit{\text{plant}}$ and $\mathit{\text{animal}}$. Enquanto uma função $\mathit{\text{mother}}:\mathit{\text{animal}}⟶\mathit{\text{animal}}$ faz sentido, uma função similar $\mathit{\text{mother}}:\mathit{\text{plant}}⟶\mathit{\text{plant}}$ usualmente não faz não faz. Lógica polissortida permite um ter termos como $\mathit{\text{mother}}(\mathit{\text{lassie}})$, mas discartar termos como $\mathit{\text{mother}}(\mathit{\text{<mrow data-mjx-texclass="ORD">my<mi mathvariant="normal">\_</mi>favorite<mi mathvariant="normal">\_</mi>oak</mrow>}})$ 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

$\mathit{\text{dog}}\subseteq \mathit{\text{carnivore}}$,

$\mathit{\text{dog}}\subseteq \mathit{\text{mammal}}$,

$\mathit{\text{carnivore}}\subseteq \mathit{\text{animal}}$,

$\mathit{\text{mammal}}\subseteq \mathit{\text{animal}}$,

$\mathit{\text{animal}}\subseteq \mathit{\text{creature}}$,

$\mathit{\text{plant}}\subseteq \mathit{\text{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 $\mathit{\text{mother}}:\mathit{\text{animal}}⟶\mathit{\text{animal}}$, e uma declaração constante $\mathit{\text{lassie}}:\mathit{\text{dog}}$, o termo $\mathit{\text{mother}}(\mathit{\text{lassie}})$ é perfeitamente válido e tem o tipo $\mathit{\text{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 $\mathit{\text{mother}}:\mathit{\text{dog}}⟶\mathit{\text{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 $\mathrm{\forall }x:p_i(x)\to 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 $\mathit{\text{list}}(X)$ pode ser declarado (with $X$ sendo um tipo paramétrico como em um template C++), e de uma declaração de subtipo $\mathit{\text{int}}\subseteq \mathit{\text{float}}$ a relação $\mathit{\text{list}}(\mathit{\text{int}})\subseteq \mathit{\text{list}}(\mathit{\text{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 $\mathit{\text{even}}\subseteq \mathit{\text{int}}$ e $\mathit{\text{odd}}\subseteq \mathit{\text{int}}$, uma declaração de termo como $\mathrm{\forall }i:\mathit{\text{int}}.(i+i):\mathit{\text{even}}$ permite declarar uma propriedade de adição de inteiros que não pode ser expressada por poliformismo ordinário.

Primeiros artigos sobre lógica de muitos tipos incluem:

• Predefinição:Citar periódico
• Predefinição:Citar periódico
• Predefinição:Citar periódico

Ligações externas

• "Many-sorted Logic", the first chapter in Lecture Notes on Decision Procedures by Calogero G. Zarba