Ementa:

• Lógica Proposicional e de Primeira ordem. Provadores automáticos de teoremas. Resolução e Tableaux semânticos. A máquina de inferência do PROLOG. Implementação de máquinas de inferência baseadas em resolução e de sistemas de tableaux para lógicas proposicional e de primeira ordem.
• Satisfatibilidade. O método Davis/Putnam. Métodos recentes. Implementações de algoritmos para SAT.
• Planejamento em IA. PDDL. Graphplan e SATplan. Métodos recentes.
• Raciocínio sobre ações. Cálculo de situações. Lógica Modal de ações.

Objetivos:

• Estudar problemas de complexidade teórica reconhecidamente difícil, e.g. NP-completo, PSPACE-completo ou EXPtime. Alguns problemas interessantes do ponto de vista prático serão estudados, em particular veremos algoritmos e estruturas de dados para estas classes de problemas. O curso será tão teórico quanto for necessário para entendimento da parte prática.

Plano de aulas:

• Aulas