Lógica Aplicada a Computação
Primeiro semestre/2013

• Veja o plano de curso.
• Antes de prosseguir (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
• Apostila:
  • Capítulo 1: Modelagem e Formalização; Capítulo 2: Lógica Proposicional
  • Capítulo 3: Lógica de Predicados até Consequência lógica
  • Capítulo 3: Lógica de Predicados/Dedução
• Slides:
  • Capítulo 1: Modelagem e Formalização
  • Capítulo 2/2.1: A realidade sob a ótica da lógica proposicional
  • Capítulo 2/2.2: A linguagem proposicional
  • Capítulo 2/2.3.1: O significado das fórmulas
  • Capítulo 2/2.3.2: Avaliação de fórmulas no nível conceitual
  • Capítulo 2/2.3.3: Equivalência lógica
  • Capítulo 2/2.3.4: Satisfabilidade, tautologias e contradições
  • Capítulo 2/2.3.5 e 2.3.6: Verificação de satisfabilidade e falseabilidade no nível conceitual. Verificação de tautologias e contradições no nível conceitual
  • Capítulo 2/2.4.1: Avaliação de fórmulas no nível formal
  • Capítulo 2/2.4.2: Verificação de satisfabilidade e falseabilidade no nível formal
  • Capítulo 2/2.4.3: Verificação de tautologias e contradições no nível formal
  • Capítulo 2/2.5: Formas normais
  • Capítulo 2/2.6: O algoritmo DPLL
  • Capítulo 2/2.7: Consequência lógica
  • Capítulo 2/2.8.1 e 2.8.2: Exemplos de regras de inferência e deduções. Sistemas dedutivos do tipo Hilbert.
  • Capítulo 2/2.8.3: Sistemas dedutivos do tipo Gentzen
  • Capítulo 2/2.8.4: Tableaux semânticos
  • Capítulo 2/2.8.5: Resolução
  • Capítulo 3/3.1 a 3.4: Lógica de Predicados até Consequência lógica
  • Capítulo 3/3.5.1 a 3.5.5: Dedução até Tableau com unificação
  • Capítulo 3/3.5.6: Resolução
  • Introdução a Prolog
• 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: fazer os 5 exercícios da Seção 2.1. Entrega: 19/3.
  • Segunda lista: 2.2: 1, 2, 3, 4; 2.3.1: 4, 5; 2.3.2: 2, 3. Entrega: 26/3.
  • Terceira lista: 2.3.3: 1, 2; 2.3.4: 2, 3, 4f, 4g, 6. Entrega: 04/4.
  • Quarta lista: 2.3.5: 2, 4; 2.3.6: 1, 2, 3, 4; 2.4.1: 1, 2, 3. Entrega: 11/4.
  • Quinta lista: 2.4.2: 1, 5, 6, 10, 11, 12; 2.4.3: 9, 10. Entrega: 02/5.
  • Sexta lista: 2.5: 1, 3, 4, 9; 2.6: 2, 4; 2.7: 3, 5. Entrega: 14/5.
  • Sétima lista: 2.8.1: 1(d, f); 2.8.2: 2, 3; 2.8.3: 1(e, j); 2.8.5: 5(b, d, f). Entrega: 04/6.
  • Oitava lista: 3.2: 2(b,d,f,h,l), 4; 3.3: 1, 2, 3, 6, 7. Entrega: 06/6.
• Soluções dos exercícios da apostila:
  • Capítulo 1.
  • Capítulo 2: Seções 2.1 a 2.3.2. (ref. às listas 1 e 2.)
  • Capítulo 2: Seções 2.3.3 a 2.4.1. (ref. às listas 3 e 4.)
  • Capítulo 2: Seções 2.4.2 e 2.4.3. (ref. à listas 5.)
  • Capítulo 2: Seções 2.5 a 2.7. (ref. à lista 6.)
  • Capítulo 2: Seções 2.8.1 a 2.8.5. (ref. à lista 7.)
  • Capítulo 2: Algumas soluções das Seções 3.1 a 3.3. (ref. à lista 8.)
• Trabalhos:
  • Primeiro trabalho: resolver alguma aplicação usando algum resolvedor SAT. Entrega: 25/4.
    Atenção: envie por email 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) sat e (2) fnc em Prolog. Entrega: 05/07/2013.
• Provas:
  • Primeira prova.
    • Data: 14/5.
    • Assunto: capítulo 2 até Seção 2.7, inclusive.
    • Para se preparar bem: veja as soluções do professor para as listas de exercícios.
    • Aqui a solução do professor.
  • Segunda prova.
    • Data: 20/06/2013. Adiada para 27/06.
    • Assunto: seções 2.7 e 2.8 do capítulo 2, e capítulo 3 da apostila.
• Veja suas notas.