Lógica Aplicada a Computação
Segundo semestre/2011

• Veja o plano de curso.
• Antes de prosseguir (e durante e depois também) ria um pouco:
  
  • Proofs from THE BOOK
    
  • Warrior
  • The Creation – part 2
  • Popular science
  • The difference (normal person v scientist)
  • Applied math (passe o mouse por cima do cartoon)
  • Windows estimation
  • Chess players
• Links importantes/interessantes:
  • Advice on writing papers
  • Automated deduction systems and groups
  • Mechanized reasoning
  • SAT Live! Up-to-date links for the SATisfiability Problem
  • SWI-Prolog
  • Mathematical Logic na Wikipedia
  • Anotações de aulas do curso Symbolic Logic de Peter Suber, (Department of Philosophy, Earlham College)
  • Livro Mathematical Logic de Stephen G. Simpson
  • Software horror stories
  • The Gödel number of the undecidable sentence
  • The International Conferences on Theory and Applications of Satisfiability Testing (SAT)
  • The international SAT Competitions web page
• Listas de exercícios:
  • Primeira lista: 1: 1, 2, 4; 2.1: 1, 2, 3. Entrega: 23/8/11. Veja uma solução.
  • Segunda lista: 2.2: 1, 2, 3; 2.3.1: 1, 2, 3, 4, 5. Entrega: 6/9/11. Veja uma solução.
  • Terceira lista: Lista do Prof. Monteiro para o dia 6/9. Veja uma solução.
  • Quarta lista: 2.3.2: 1, 2, 3; 2.3.3: 1, 3, 5; 2.3.4: 1, 2. Entrega: 29/9/11. Veja uma solução.
  • Quinta lista: 2.3.5: 1, 3, 4, 6, 7. Entrega: 04/10/11. Veja uma solução.
  • Sexta lista: 2.3.6: 2(c,e,f), 3(c,e,f), 5(c,e,f), 6(c,e,f); 2.3.7: 1(a,c,d), 2 . Entrega: 13/10/11.
  • Sétima lista: 2.3.8: 3(a,f), 5, 6, 9; 2.3.9: 2, 3, 4. Entrega: 01/11/11.
  • Oitava lista: 2.5.1: 1(b,e); 2.5.3: 1(b,e); 2.5.4: 1(b,e); 2.5.5: 2(b,e). Entrega: 17/11/11.
• Trabalhos:
  • Primeiro trabalho: resolver alguma aplicação usando algum resolvedor SAT. Entrega: 31/10/11. Adiada para o dia 10/11/11.
    Atenção: enviei por e-mail programas e relatório e entregue uma cópia do relatório em papel.
    Algumas aplicações, tendo em vista o primeiro trabalho (leia, primeiro, o cap. 1 da 11a. publicação):
    1. A SAT Approach to Query Optimization in Mediator Systems
    2. A SAT-based approach to decipher Gene Regulatory Networks
    3. A SAT Encoding for the Social Golfer Problem
    4. Applications of SAT Solvers to Cryptoanalysis of Hash Functions
    5. Boolean Satisfiability in Electronic Design Automation
    6. Diagnosis of Discrete-Event Systems Using Satisfiability Algorithms
    7. Efficient haplotype inference with Boolean satisfiability
    8. Encoding Plans in Propositional Logic
    9. Improving the Encoding of LTL Model Checking into SAT
    10. Practical Applications of Boolean Satisfiability
    11. Propositional Satisfiability - Techniques, Algorithms and Applications
    12. SAT in Bioinformatics - Making the Case with Haplotype Inference
    13. SAT-based Verification Methods and Applications in Hardware Verification
    14. Satisfiability-Based Program Reasoning and Program Syntesis
    15. School Timetabling using Satisfiability Solvers
    16. Sudoku as a SAT problem
    17. Test Pattern Generation Using Boolean Satisfiability
  • Segundo trabalho: (1) macaco e bananas e (2) sat em Prolog. Entrega: 01/12/11.
• Provas:
  • Primeira prova. (Prova para aluno de graduação que preferiu fazer depois da SConh.)
    • Data: 18/10/2011.
    • Assunto: capítulo 1 e seções 2.1 a 2.3 (esta última até 2.3.7) do capítulo 2 da apostila.
    • Para se preparar bem: veja as soluções do professor para as listas de exercícios.
  • Segunda prova. Valor: 13 pontos.
    • Data: 01/12/2011. Note: no dia 29/11 não haverá aula.
    • Assunto: capítulo 2, seção 2.3.8 em diante, e capítulo 3 da apostila.
    • Exercícios do cap. 3 preparatórios para a prova: 3.2: 1; 3.3.1: 1,2,3; 3.4: 1; 3.4:1; 3.5.3: 1; 3.5.4: 1; 3.5.5: 3; 3.5.7: 1,2,3.
  • Exame especial.
    • Data: 14/12/2011, às 10h.
    • Local: sala 4023.
    • Assunto: toda a matéria vista em aulas.
    • Inscrição: para fazer o exame, faça sua inscrição até dia 12/12 enviando-me um email.
• Veja suas notas.