Conclusão

Computação e Complexidade

• Qual o efeito do número de proposições no algoritmo da resolução?
• Qual o efeito do número de átomos em SAT?
• $\cat{P} \stackrel{?}{=} \cat{NP}$ isto é, resolver vs. decidir.
  • Resolver: Calcular $x$ tal que $x \times 7 = 56$.
  • Decidir: Verificar se $8 \times 7 = 56$.

Expressividade

• No Labirinto do Minotauro, como descrever um labirinto com $n \times m$ salas?
• Em geral, quantas regras de dedução são necessárias?

Objetos e Relações (antevisão)

• $\fat{Minotauro}{12}$.
• $\forall x~\fat{Brisa}{x} \liff \exists y~\fat{Adjacente}{x, y} \land \fat{Poço}{y}$.