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{𝑝𝑙𝑎𝑛𝑡}}$ and $\mathit{\text{𝑎𝑛𝑖𝑚𝑎𝑙}}$. Enquanto uma função $\mathit{\text{𝑚𝑜𝑡ℎ𝑒𝑟}}:\mathit{\text{𝑎𝑛𝑖𝑚𝑎𝑙}}⟶\mathit{\text{𝑎𝑛𝑖𝑚𝑎𝑙}}$ faz sentido, uma função similar $\mathit{\text{𝑚𝑜𝑡ℎ𝑒𝑟}}:\mathit{\text{𝑝𝑙𝑎𝑛𝑡}}⟶\mathit{\text{𝑝𝑙𝑎𝑛𝑡}}$ usualmente não faz não faz. Lógica polissortida permite um ter termos como $\mathit{\text{𝑚𝑜𝑡ℎ𝑒𝑟}}(\mathit{\text{𝑙𝑎𝑠𝑠𝑖𝑒}})$, mas discartar termos como $\mathit{\text{𝑚𝑜𝑡ℎ𝑒𝑟}}(\mathit{\text{<mrow data-mjx-texclass="ORD">𝑚𝑦<mi mathvariant="normal">\_</mi>𝑓𝑎𝑣𝑜𝑟𝑖𝑡𝑒<mi mathvariant="normal">\_</mi>𝑜𝑎𝑘</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{𝑑𝑜𝑔}}\subseteq \mathit{\text{𝑐𝑎𝑟𝑛𝑖𝑣𝑜𝑟𝑒}}$,

$\mathit{\text{𝑑𝑜𝑔}}\subseteq \mathit{\text{𝑚𝑎𝑚𝑚𝑎𝑙}}$,

$\mathit{\text{𝑐𝑎𝑟𝑛𝑖𝑣𝑜𝑟𝑒}}\subseteq \mathit{\text{𝑎𝑛𝑖𝑚𝑎𝑙}}$,

$\mathit{\text{𝑚𝑎𝑚𝑚𝑎𝑙}}\subseteq \mathit{\text{𝑎𝑛𝑖𝑚𝑎𝑙}}$,

$\mathit{\text{𝑎𝑛𝑖𝑚𝑎𝑙}}\subseteq \mathit{\text{𝑐𝑟𝑒𝑎𝑡𝑢𝑟𝑒}}$,

$\mathit{\text{𝑝𝑙𝑎𝑛𝑡}}\subseteq \mathit{\text{𝑐𝑟𝑒𝑎𝑡𝑢𝑟𝑒}}$,

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{𝑚𝑜𝑡ℎ𝑒𝑟}}:\mathit{\text{𝑎𝑛𝑖𝑚𝑎𝑙}}⟶\mathit{\text{𝑎𝑛𝑖𝑚𝑎𝑙}}$, e uma declaração constante $\mathit{\text{𝑙𝑎𝑠𝑠𝑖𝑒}}:\mathit{\text{𝑑𝑜𝑔}}$, o termo $\mathit{\text{𝑚𝑜𝑡ℎ𝑒𝑟}}(\mathit{\text{𝑙𝑎𝑠𝑠𝑖𝑒}})$ é perfeitamente válido e tem o tipo $\mathit{\text{𝑎𝑛𝑖𝑚𝑎𝑙}}$. 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{𝑚𝑜𝑡ℎ𝑒𝑟}}:\mathit{\text{𝑑𝑜𝑔}}⟶\mathit{\text{𝑑𝑜𝑔}}$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{𝑙𝑖𝑠𝑡}}(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{𝑖𝑛𝑡}}\subseteq \mathit{\text{𝑓𝑙𝑜𝑎𝑡}}$ a relação $\mathit{\text{𝑙𝑖𝑠𝑡}}(\mathit{\text{𝑖𝑛𝑡}})\subseteq \mathit{\text{𝑙𝑖𝑠𝑡}}(\mathit{\text{𝑓𝑙𝑜𝑎𝑡}})$ é 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{𝑒𝑣𝑒𝑛}}\subseteq \mathit{\text{𝑖𝑛𝑡}}$ e $\mathit{\text{𝑜𝑑𝑑}}\subseteq \mathit{\text{𝑖𝑛𝑡}}$, uma declaração de termo como $\mathrm{\forall }i:\mathit{\text{𝑖𝑛𝑡}}.(i+i):\mathit{\text{𝑒𝑣𝑒𝑛}}$ 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