Conclusão

A Lógica de Primeira Ordem é muito mais expressiva do que a Lógica Proposicional.

O uso de termos e relações permite uma escrita mais compacta (os exemplos do LdM) e geral (ainda no LdM)

SAT é insolúvel para a LPO.

Não existe um algoritmo geral para decidir quando uma fórmula tem um modelo.

Há limites aos domínios e relações que a LPO que pode descrever.

• A existência de caminho entre dois vértices de um grafo orientado (Reachability problem na wikipedia) não pode ser expressa por uma fórmula da LPO.
• O Princípio de Indução na Linguagem dos Números Naturais.

Porém, é realizável especificar e verificar modelos de muitas linguagens de primeira ordem.

Aplicações da LPO incluem:

• Estruturas de dados (conjuntos, listas, etc)
• Especificação de Tarefas.
• Representação de Conhecimento.
• Verificação de Programas.