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?
• $\mathcal{P}\stackrel{?}{=}\mathcal{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)

• $\text{Minotauro}\left(12\right)$.
• $\forall x\text{Brisa}\left(x\right)\leftrightarrow \exists y\text{Adjacente}\left(x,y\right)\wedge \text{Poc¸o}\left(y\right)$.