AULA 25
19 Dezembro 2017, 10:30 • Fernando Ferreira
Resolução do problema do terceiro mini-teste sobre o algoritmo de unificação mais geral (mgu). Regras para obter uma forma prenexa duma fórmula. Alguns comentários. Deduções formais com múltiplas quantificações: um exemplo e uma falácia.
A noção de verdade de Tarski (verdade duma sentença numa estrutura para a linguagem). A noção de consequência (semântica) FO (first-order). A noção de consequência (sintática) dada pelo sistema de regras de Fitch. O teorema da completude de Gödel diz que as duas noções coincidem.
Uff...