Fundamentos Lógicos da IA - 2025-1
UnB-\(\gamma\)

Table of Contents

Table of Contents

1. Material Didático e conteúdo programático (preliminar)

  1. Introdução
  2. Introdução à lógica clássica
  3. Lógica de primeira ordem
  4. Representações proposicionais
  5. Procedimentos automáticos de prova
  6. Problema de satisfatibilidade (SAT)
  7. Algoritmos para SAT
  8. Busca em grafos e/ou
  9. Formas não clausais de representação
  10. Planejamento
    • Aplicações em planejamento \(1\)

2. Plano de aulas

2.1. Aula 1   25_mar

2.2. Aula 2   27_mar

  • Agentes Lógicos
    • Capítulo 7 AI: A modern approach

2.3. Aula 3   01_abr

  • Continuação Agentes Lógicos

2.4. Aula 4   03_abr

  • Continuação Agentes Lógicos
  • (previsão) Especificação Trabalho 1 - peso X

2.5. Aula 5   08_abr

  • Lógica de Primeira Ordem

2.6. Aula 6   10_abr

  • Lógica de Primeira Ordem

2.7. Aula 7   15_abr

  • Planejamento Clássico

2.8. Aula 8   17_abr

  • Planejamento Clássico

2.9. Aula 9   22_abr

  • PDDL

2.10. Aula 10   24_abr

  • PDDL
  • Exercícios PDDL no MOJ (não vale nota)

2.11. Aula 11   29_abr

  • Planejadores
  • (previsão) Especificação Trabalho 2 - peso Y

2.12. Aula 12   01_mai feriado

2.13. Aula 13   06_mai

  • NP-completude

2.14. Aula 14   08_mai

  • NP-completude

2.15. Aula 15   13_mai

  • Satisfatibilidade Booleana

2.16. Aula 16   15_mai

  • Codificação CNF

2.17. Aula 17   20_mai

  • Algoritmos Completos

2.18. Aula 18   22_mai

  • CDCL Solvers

2.19. Aula 19   27_mai

  • CDCL Solvers

2.20. Aula 20   29_mai

  • Heurísticas de Ramificação
  • (previsão) Especificação da GRANDE COMPETIÇÃO! - Trabalho peso P

2.21. Aula 21   03_jun

  • Planejamento e SAT

2.22. Aula 22   05_jun

  • Planejamento e SAT

2.23. Aula 23   10_jun

  • Planejamento e SAT
  • (previsão) Especificação Trabalho 3 - peso B

2.24. Aula 24   12_jun

  • Planejamento e SAT

2.25. Aula 25   17_jun

  • Planejamento e SAT

2.26. Aula 26   19_jun feriado

2.27. Aula 27   24_jun

  • Model Counting

2.28. Aula 28   26_jun

  • Pseudo-Boolean e restrições de cardinalidade

2.29. Aula 29   01_jul

  • Pseudo-Boolean e restrições de cardinalidade
  • (previsão) Especificação trabalho 4 - peso Z

2.30. Aula 30   03_jul

  • Busca Competitiva

2.31. Aula 31   08_jul

  • Busca Competitiva

2.32. Aula 32   10_jul

  • Busca Competitiva
  • (previsão) Especificação trabalho 5 - peso K

2.33. Aula 33   15_jul

  • Problema de Satisfação de Restrição

2.34. Aula 34   17_jul

  • Problema de Satisfação de Restrição

2.35. Aula 35   22_jul

  • Problema de Satisfação de Restrição

2.36. Aula 36   24_jul

  • Apresentação do GRANDE resultado da competição
    • transmissão no youtube ao vivo
    • apresentação das melhores soluções
    • premiação

3. Plano de Ensino

O plano de ensino completo poder ser baixado AQUI.

O plano de ensino e plano de aulas é um PLANO e pode sofrer modificações ao longo do semestre de acordo com o rendimento da turma.

3.1. Método

Aula expositiva por meio de aula síncronas em Sala de Aula, quadro branco e projetor, lista de exercícios e, material de apoio disponibilizado no Youtube (gravados ou em live stream).

Os slides das aulas; materiais, e; trabalhos estarão disponíveis na página https://www.brunoribas.com.br/flia/2025-1/ . Os demais materiais estarão disponíveis no SIGAA.

Toda a comunicação será dada em SALA de AULA e noticiada no SIGAA como uma notícia da disciplina.

3.2. Critérios de Avaliação

  • A avaliação será composta por um conjunto de trabalhos, com pesos variáveis.
    • Os trabalhos funcionarão como checkpoints ao longo da disciplina, auxiliando na consolidação dos conteúdos estudados.
    • Alguns trabalhos serão realizados durante o horário de aula e abrangerão os tópicos mais recentes.
  • As notas serão expressas como um número inteiro no intervalo \([0,100]\).
    • Cada trabalho terá um peso definido no momento de sua divulgação.
  • As avaliações poderão conter questões teóricas e/ou práticas, conforme critério do professor.
  • Qualquer tentativa de fraude (cola, cópia ou uso indevido de LLM) resultará em média ZERO no semestre para todos os envolvidos, acarretando menção SR.

3.2.1. Trabalhos

Os trabalhos poderão ser organizados em três modalidades principais:

  1. Trabalhos com prazo estendido: possuem um período de até 1 mês para conclusão e podem envolver caráter competitivo. A entrega será realizada por meio do sistema MOJ, e os melhores trabalhos poderão ser selecionados para apresentação da solução desenvolvida.
  2. Trabalhos em sala de aula: definidos em um encontro e finalizados na aula seguinte ou nas subsequentes.
    • Para os trabalhos em grupo, alunos ausentes na aula de definição devem apresentar sua equipe na aula imediatamente seguinte.
    • Caso um estudante falte no dia da finalização, poderá solicitar um prazo adicional equivalente ao tempo de uma aula, desde que apresente um atestado de saúde em até 5 (cinco) dias.
  3. Trabalhos de apresentação: estruturados em duas etapas dentro de uma única aula.
    • Na primeira parte, os alunos estudam o conteúdo proposto.
    • Na segunda parte, apresentam suas conclusões para a turma.
    • A participação de todos os integrantes do grupo é obrigatória. O professor poderá selecionar um dos membros para realizar a apresentação.
    • Estudantes ausentes receberão nota Zero.
  • Se o estudante utilizar modelos de linguagem treinados (LLMs) para gerar parte do trabalho, incluindo código ou texto, essa utilização deve ser declarada explicitamente.
    • O não cumprimento dessa exigência pode ser interpretado como tentativa de fraude.
  • O professor poderá, a seu critério, convocar alunos para que defendam o trabalho em caso de suspeita de uso indevido de LLM e/ou cópia (seja de outro aluno ou da internet)
    • A apresentação será em caráter de defesa podendo ser solicitado modificações no trabalho ou reimplementação de trechos do código.

Nos trabalhos realizados em sala, um aluno que se ausentar poderá solicitar uma nova data para realizar um trabalho equivalente, desde que apresente um atestado de saúde em até 5 (cinco) dias. Essas reposições ocorrerão entre 18h00 e 19h50 nos dias letivos da disciplina.

3.2.2. Presença

A presença será registrada por meio de lista de assinaturas ou chamada oral conduzida pelo professor.

3.2.3. Menção Final

As notas serão calculadas conforme a equação abaixo:

\begin{align} M_F = \frac{ \sum_{i=0}^{N}(K_i * T_i)}{\sum_{i=0}^{N}(K_i)} \end{align}
  • Onde \(K_i\) são os pesos das atividades. Os pesos serão divulgados pelo professor no momento da divulgação da atividade

3.2.4. Critérios de aprovação

Obterá aprovação no curso o aluno que cumprir todas as exigências listadas abaixo:

  1. \(M_F >= 50\); e
  2. Presença em \(75\%\) ou mais das aulas.

Por fim, a menção final do curso é dada de acordo com a tabela abaixo:

\(M_F\) Menção Descrição
\(0\) SR Sem rendimento
\([1,29]\) II Inferior
\([30,49]\) MI Médio Inferior
\([50,69]\) MM Médio
\([70,89]\) MS Médio Superior
\([90,100]\) SS Superior

IMPORTANTE: Atestados médicos e documentos comprobatórios de justificativa de faltas dão direito à realização de atividades avaliativas que você venha a perder, mas essas ausências justificadas também são levadas em consideração como ausências efetivas para o cômputo da frequência mı́nima obrigatória (Graduação UnB – Manual para estudantes, pág. 35).

3.3. Bibliografia

  • Biere, Armin; Heule, Marijn J. H.; van Maaren, Hans; Walsh, Toby Handbook of Satisfiability, 2009.
  • Chang, Chin-Liang; Lee, Richard Char-Tung Symbolic logic and mechanical theorem proving. San Diego, CA: Academic Press, 1987.
  • Darwiche, A.; Marquis, P. A knowledge compilation map. JAIR, 2002.
  • Haslum, Patrik; Lipovetzky, Nir; Magazzeni, Daniele; Muise, Christian An Introduction to the Planning Domain Definition Language. Springer, 2019.
  • Marek, Victor W. Introduction to Mathematics of Satisfiability, CRC Press, 2009.
  • Mendelson, Elliott Introduction to Mathematical Logic (5a edição), CRC Press, 2010.
  • Montano, RANR; Ribas, BC Planning as Mixed-Horn Formulas Satisfiability, 2017.
  • Ribas, Bruno C Um método de pré-processamento de fórmulas SAT e pseudo-boolean baseado em técnicas de programação linear inteira mista, 2015.
  • Ribas, Bruno C; Suguimoto, RM; Montano, RANR; Silva, F; Bona, LCE; Castilho, M On modelling virtual machine consolidation to pseudo-Boolean constraints, 2012.
  • Ribas, Bruno C; Suguimoto, RM; Montano, RANR; Silva, F; Bona, LCE; Castilho, M PBFVMC: A New Pseudo-Boolean Formulation to Virtual-Machine Consolidation, 2013.
  • Russell, Stuart; Norvig, Peter Artificial Intelligence: A Modern Approach, 2020.
  • Artificial Intelligence: A Modern Approach. 3a Ed. S. Russell e P. Norvig. (cap 7, slides).
  • Planning.Wiki - The AI Planning & PDDL Wiki

4. Monitor

Não teremos monitores neste semestre

5. Presença

  • Publicado diretamente no SIGAA

6. Notas

6.1. Trabalhos que valem nota

6.2. Consolidadas

Author: Bruno Ribas

Created: 2025-03-27 Thu 10:08

Validate