Mostrar código-fonte de Regra de inferência

{{Sem fontes|data=maio de 2022}}
'''Inferência''' é o processo pelo qual se chega a uma [[proposição]], firmada na base de uma ou outras mais [[proposição|proposições]] aceitas como ponto de partida do processo. O [[Argumento]] é chamado de premissa e o valor de conclusão. As conclusões são deduzidas a partir das premissas. Caso o estado das premissas esteja vazio, então a conclusão é dita ser o axioma da lógica.

Uma propriedade desejável de uma regra de inferência é que esta seja efetiva, isto é, existe um procedimento efetivo para determinar se uma dada fórmula é inferível de um dado conjunto de fórmulas.

'''Regras de inferência''' têm as seguintes características:
# Se a Hipótese for verdadeira, então a Conclusão é verdadeira;
# Verificação de tipos é baseada em inferência. Se E1 e E2 tem certos tipos, então E3 tem um certo tipo;
# Regras de inferência são uma notação compacta para comandos de implementação;
# Inicia-se com um sistema simplificado de regras ao qual adiciona-se novas características gradualmente;
# As premissas são regras sem hipóteses.

Uma regra de inferência não precisa preservar qualquer propriedade [[semântica]] como verdadeira, já que não existe nenhuma regra que garanta que uma caracterização lógica sintática tenha uma semântica. Uma regra pode preservar, por exemplo, a propriedade da conjunção de uma sub-fórmula da uma fórmula mais extensa do conjunto de premissas.

Note que existem diferentes sistemas de lógicas formais, cada qual com seus próprios conjuntos de fórmulas bem-formadas, regras de inferências, e algumas vezes, semânticas. Tome como exemplo as lógicas temporal, modal ou intuicionista. Na [[lógica de primeira ordem]], é necessária uma regra de inferência adicional, conhecida como generalização.

Na lógica formal, as regras de inferência são normalmente determinadas nas seguinte forma:<br />
premissa #1<br />
premissa #2<br />
...<br />
premissa #n<br />
____________<br />
conclusão

Esta expressão indica, que sempre que as premissas dadas forem obtidas durante alguma derivação lógica, a conclusão especificada pode ser provada. A linguagem formal que é usada para descrever ambas premissas e conclusões depende do atual contexto das derivações. Por exemplo, pode ser usada como uma fórmula lógica, assim como em

&nbsp;&nbsp;A→B

<u>&nbsp;&nbsp;A &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;</u>

&nbsp;&nbsp;∴B

ao qual é justamente a regra modus ponens da [[lógica proposicional]]. Regras de inferência são freqüentemente formuladas como regras esquematizadas pelo uso de variáveis universais. Na regra (esquemática) acima. A e B podem ser substituídas por algum elemento do universo (ou às vezes, por convenção, alguns sub-conjuntos restritos como as proposições) um conjunto infinito de regras de inferência.

Um sistema de prova é formado por um conjunto de regras, as quais podem ser interligadas para formar provas, ou derivações. Uma derivação tem apenas uma conclusão, a qual é um enunciado provado ou derivado. Se a premissa for verdadeira, então a conclusão também o será.

== Admissibilidade e Derivabilidade ==
Em um conjunto de regras, uma regra de inferência pode ser redundante no sentido de que ela pode ser admissível ou derivável. Uma regra derivável é aquela que a conclusão pode ser derivada de suas premissas usando outras regras. Uma regra admissível é aquela que a conclusão é verdadeira sempre que as premissas também o forem. Todas as regras deriváveis são admissíveis. Para observar a diferença, considere os seguintes conjuntos de regras para definir os números naturais (tome <math>n\,\,\mathsf{nat}</math> como <math>n</math> pertencendo ao conjunto dos números naturais).

<math>
\begin{matrix}
\frac{}{\mathbf{0} \,\,\mathsf{nat}} &
\frac{n \,\,\mathsf{nat}}{\mathbf{s(}n\mathbf{)} \,\,\mathsf{nat}} \\
\end{matrix}
</math>

A primeira regra indica que '''0''' é um número natural, e o segundo indica que '''s(n)''' é um número natural se ''n'' também o for. Em um sistema de provas, a regra a seguir demonstra que o segundo sucessor de um número natural é também um número natural, é derivável:

<math>
\frac{n \,\,\mathsf{nat}}{\mathbf{s(s(}n\mathbf{))} \,\,\mathsf{nat}}
</math>

Estas derivações são apenas composições de dois usos da regra de sucessão acima. A regra a seguir para a afirmação da existência de um antecessor para algum número diferente de zero é meramente admissível:

<math>
\frac{\mathbf{s(}n\mathbf{)} \,\,\mathsf{nat}}{n \,\,\mathsf{nat}}
</math>

Este é um fato dos números naturais, como pode ser provado por [[Indução#Matemática|indução]] (para provar que esta regra é admissível, uma delas deve assumir uma derivação da premissa, e induzir para produzir uma derivação de <math>n \,\,\mathsf{nat}</math>). Entretanto, ele não é '''derivável''', porque ele depende de uma estrutura da derivação da premissa. Pelo fato desta derivabilidade ser estável sob adições para um sistema de provas, a admissibilidade não o é. Para ver a diferença, suponha que a seguinte regra sem sentido fosse adicionada para o sistema de provas:

<math>
\frac{}{\mathbf{s(-3)} \,\,\mathsf{nat}}
</math>

Neste novo sistema, a regra da dupla sucessão ainda é derivável. Entretanto, a regra para achar o antecessor já não é admissível, pois não há como derivar <math>\mathbf{-3} \,\,\mathsf{nat}</math>. A fragilidade da admissibilidade vem da maneira como é provada: desde que a prova possa induzir na estrutura das derivações das premissas, extensões para o sistema adicionam novos casos para esta prova, a qual pode já não ser mais válida.

Regras admissíveis podem ser pensadas como teoremas de sistemas de provas. Por exemplo, no cálculo seqüencial onde o teorema do corte é válido, a '''regra do corte''' é admissível.

== Outras Considerações ==
Regras de inferências podem também ser indicadas desta forma:
1. algumas (talvez nenhuma) premissas.
2. o símbolo <math> \vdash</math> "infere", "prova" ou "conclui".
3. uma conclusão.

Isto geralmente uma visão relacional (oposto de funcional) de uma regra de inferência, onde o <math> \vdash</math> mantém uma relação de dedução entre premissas e conclusões.

Regras de inferência devem ser distinguidas de axiomas de uma teoria. Em termos de semântica, axiomas são asserções válidas. Axiomas são considerados pontos iniciais para a aplicação de regras de inferência e geração de um conjunto de conclusões. Ou em termos informais:

Regras são enunciados SOBRE o sistema, axiomas são enunciados no sistema. Por exemplo:

A regra que de <math>\vdash p</math> você pode inferir que <math>\vdash</math> '''Derivável(p)''' é um enunciado que diz que se você pode provar p, então é provável que p seja derivável. Isto é usado na aritmética de Peano, por exemplo.

O axioma '''Derivável(p)''' pode significar que todo enunciado verdadeiro é derivável. Isto, entretanto, não é usado na aritmética de Peano.

Regras de inferência possuem um papel vital na especificação do cálculo lógico tanto na teoria de prova quanto no cálculo sequencial e na dedução natural.

== Ver também ==
* [[Axioma]]
* [[Lista de regras de inferência|Lista de Regras de Inferência]]

== Ligações externas ==
* {{Link|pt|2=http://pucrs.campus2.br/~annes/inflog_aula6.html/ |3=PUC-RS}}
* {{Link||2=http://people.hofstra.edu/Stefan_Waner/realworld/logic/logic5.html/ |3=Hofstra}}
* {{Link|pt|2=http://www.lasid.ufba.br/graduacao/compiladores/L-semantica-formal-intro.pdf/ |3=UFBA}}

{{DEFAULTSORT:Regra Inferencia}}
[[Categoria:Regras de inferência| ]]