Computação

Problemas Computacionais da Lógica de Primeira Ordem

Em relação à lógica proposicional, aqui apenas se substitui "proposição" por "fórmula" e "valoração" por "interpretação".

Definição (SAT)

O problema da satisfação (SAT) consiste no conjunto de pares $(p,b)$ em que $p$ é uma fórmula e $b$ um valor booleano tal que $$b=\{\begin{array}{ll}\mathtt{v}& \text{se}\exists v\left(v\models p\right)\\ \mathtt{f}& \text{caso contraˊrio}\end{array}$$

Isto é, Determinar se uma fórmula data tem algum modelo.

Nos tipos de fórmulas, uma fórmula que tenha algum modelo é compatível ou satisfazível.

Definição (Validade)

O problema da validade consiste no conjunto de pares $(p,b)$ em que $p$ é uma fórmula e $b$ um valor booleano tal que $$b=\{\begin{array}{ll}\mathtt{v}& \text{se}\forall v\left(v\models p\right)\\ \mathtt{f}& \text{caso contraˊrio}\end{array}$$

Isto é, Determinar se uma fórmula dada é válida.

Nos tipos de fórmulas, para uma fórmula válida (tautologia) todas as interpretações são modelos.

Definição (Provabilidade)

O problema da provabilidade consiste no conjunto de pares $(p,b)$ em que $p$ é uma fórmula e $b$ um valor booleano tal que $$b=\{\begin{array}{ll}\mathtt{v}& \text{se}⊢p\\ \mathtt{f}& \text{caso contraˊrio}\end{array}$$

Isto é, Determinar se uma fórmula data tem uma prova.

Um teorema é uma fórmula que tem uma prova (sem hipóteses).

(In)Decidibilidade

Na lógica de primeira ordem o problema SAT é indecidível.

• Na lógica proposicional, existe um algoritmo (não eficiente) que decide se uma proposição é, ou não, satisfazível.
• Na lógica de primeira ordem nenhum algoritmo decida, em geral, se uma fórmula é, ou não, satisfazível.
• Ao contrário do problema SAT proposicional, em que não se sabe se existe um algoritmo eficiente, sobre o SAT de primeira ordem sabe-se que não existe um algorimo, eficiente ou não.

Demonstrar estas afirmações está fora do âmbito desta disciplina.

• Conhecem-se algoritmos para SAT em classes grandes de fórmulas, mas nenhum tem toda a generalidade.
• Este assunto é referido na página do Post Correspondence Problem na wikipedia.

Verificação por Modelos

• A maior expressividade da Lógica de Primeira Ordem em relação à Lógica Proposicional sacrifica a decidibilidade de SAT.
• Ainda assim, As Amigos de Gandalf mostram que com a verificação de modelos é possível resolver problemas práticos de modelação.