Lógica para Computação - Turmas S71 e S73 - 2009.1
De Wiki DAINF
(Diferença entre revisões)
(→Material para os Trabalhos) |
(→Material para os Trabalhos) |
||
(129 edições intermediárias de 8 usuários não apresentadas) | |||
Linha 1: | Linha 1: | ||
− | == Assuntos e Equipes == | + | Informações sobre o oferecimento da disciplina [[Lógica para Computação]] em 2009.1. |
+ | |||
+ | == [[Projeto Integrado - Turma S73 - 2009.1]] == | ||
+ | |||
+ | == [[Projeto Final - Turma S71 - 2009.1]] == | ||
+ | |||
+ | == Assuntos e Equipes das Apresentações == | ||
=== Engenharia de Computação (S71) === | === Engenharia de Computação (S71) === | ||
− | # Axiomatização: Vinícius, Daniel e André | + | # [[Axiomatização: Vinícius, Daniel e André]] |
− | # Dedução Natural: | + | #* 24/03/2009 |
+ | #* Equipe debatedora: 12 | ||
+ | # [[Dedução Natural: Alexandre, Liège e Danilo]] | ||
+ | #* 24/03/2009 | ||
+ | #* Equipe debatedora: 11 | ||
# Tablôs Analíticos: Rebeca, Líria e Cristiane | # Tablôs Analíticos: Rebeca, Líria e Cristiane | ||
− | # Tablôs KE: Lucas, Demétrius e | + | #* 25/03/2009 |
+ | #* Equipe debatedora: 10 | ||
+ | # Tablôs KE: Lucas, Demétrius e João | ||
+ | #* 25/03/2009 | ||
+ | #* Equipe debatedora: 9 | ||
# Formas Normais: Kelvin, Dalton e Jorge | # Formas Normais: Kelvin, Dalton e Jorge | ||
+ | #* 31/03/2009 | ||
+ | #* Equipe debatedora: 8 | ||
# Resolução Proposicional: Henrique P., Cibele e Amanda | # Resolução Proposicional: Henrique P., Cibele e Amanda | ||
− | # Substituição: Felipe Lisboa e | + | #* 01/04/2009 |
+ | #* Equipe debatedora: 7 | ||
+ | # Substituição e Unificação: Felipe Lisboa, Victor Perales e Bruno Bellucci | ||
+ | #* 15/04/2009 | ||
+ | #* Equipe debatedora: 1 | ||
# Lógicas Não Clássicas: Eduardo Bonet, Tiago e Jean | # Lógicas Não Clássicas: Eduardo Bonet, Tiago e Jean | ||
+ | #* 28/04/2009 | ||
+ | #* Equipe debatedora: '''14''' | ||
# Ontologias: Márcio, Cláudio, Henrique Rein. | # Ontologias: Márcio, Cláudio, Henrique Rein. | ||
− | # | + | #* 05/05/2009 |
− | # Programação em Lógica: Augusto, Guilherme, | + | #* Equipe debatedora: '''13''' |
− | # | + | # Programação em Lógica: Augusto, Guilherme, Marlon Bill |
− | # | + | #* 06/05/2009 |
+ | #* Equipe debatedora: 5 | ||
+ | # Z, uma linguagem de Especificação: Suleiman, Rafael, Julio, Luiz | ||
+ | #* 12/05/2009 | ||
+ | #* Equipe debatedora: 4 | ||
# Ontologias e Web Semântica (com lógicas de descrição): Marcos, André, Maurício | # Ontologias e Web Semântica (com lógicas de descrição): Marcos, André, Maurício | ||
+ | #* 13/05/2009 | ||
+ | #* Equipe debatedora: 3 | ||
+ | # VDM-SL, uma linguagem de especificação: Fabio César, Eduardo Rachid e Cleverson | ||
+ | #* 19/05/2009 | ||
+ | #* Equipe debatedora: '''6''' | ||
+ | # Provador de teorema - Otter: André Luiz, Gionatta e Pedro. | ||
+ | #* 20/05/2009 | ||
+ | #* Equipe debatedora: '''2''' | ||
+ | |||
+ | === Bacharelado em Sistemas de Informação (S73) === | ||
+ | |||
+ | # [[Axiomatização: Lucas Campos Silva, Marcelo Butzke Leopoldino, Isaac Toyoshi Takiguchi Jr.]] | ||
+ | #* 25/03/2009 | ||
+ | #* Equipe debatedora: 14 | ||
+ | # Dedução Natural: Rubens Carlos Meggetto Junior, Estevan Frederico Pasquetta Jantsk, Thomaz Teodorovicz | ||
+ | #* 25/03/2009 | ||
+ | #* Equipe debatedora: 13 | ||
+ | # Tablôs Analíticos: Daniel Felipe Warkentin, Raul Vitor Tessaro Esteves | ||
+ | #* 01/04/2009 | ||
+ | #* Equipe debatedora: 12 | ||
+ | # Tablôs KE: Cristiano De Oliveira Viana Correia, Jonatas Da Luz, Luan Nestor Vageti Aruquipa | ||
+ | #* 03/04/2009 | ||
+ | #* Equipe debatedora: 11 | ||
+ | # [[Formas Normais: Emerson Shigueo Sugimoto, Rodrigo Cirino De Andrade, Vagner Vengue]] | ||
+ | #* 22/04/2009 | ||
+ | #* Equipe debatedora: 10 | ||
+ | # Resolução Proposicional: Ana Paula Ferreira, Fernando Bozza, Vanessa Maria Da Silva | ||
+ | #* 29/04/2009 | ||
+ | #* Equipe debatedora: 9 | ||
+ | # Substituição e Unificação: Bruno Milczewski, Mario Sergio Esperanca Silva, Thiago Vinicius Pereira | ||
+ | #* 06/05/2009 | ||
+ | #* Equipe debatedora: 1 | ||
+ | # Lógicas Não Clássicas: Andressa Caroline Portes Da Cunha, Melina Deraldo Dos Santos, Thays Boiko | ||
+ | #* 08/05/2009 | ||
+ | #* Equipe debatedora: 2 | ||
+ | # Ontologias: Fernando Hiroshi Suemitsu, Bruno Guilherme Andretta De Miranda, Matheus Alves De Souza | ||
+ | #* 13/05/2009 | ||
+ | #* Equipe debatedora: 3 | ||
+ | # Provadores de Teoremas - Visão geral: Andrei Magaievski, Andre Luiz De Lacerda, Ricardo Trizzolini Piekarski | ||
+ | #* 15/05/2009 | ||
+ | #* Equipe debatedora: 4 | ||
+ | # Programação em Lógica: Andre Hoeldtke Castro, Rafael Oliveira Tavares Pinto, Vinicius Andreatta | ||
+ | #* 20/05/2009 | ||
+ | #* Equipe debatedora: 8 | ||
+ | # A linguagem de especificação Z: Bruna Pereira Segan, Leticia Ueda, Kelly Cristina Schultz | ||
+ | #* 22/05/2009 | ||
+ | #* Equipe debatedora: 7 | ||
+ | # Um provador de teoremas - KEMS: Eduardo Carvalho Zanello, Gregorio Ivanchechen De Mattos, Pablo Kravicz, Ana Cristina Da Silva | ||
+ | #* 27/05/2009 | ||
+ | #* Equipe debatedora: 6 e '''5''' | ||
+ | <!-- | ||
+ | # A linguagem de especificação VDM: Carlos Henrique De Paula | ||
+ | !#* 24/04/2009 | ||
+ | !#* Equipe debatedora: 5 | ||
+ | --> | ||
== Material para os Trabalhos == | == Material para os Trabalhos == | ||
Linha 25: | Linha 106: | ||
# Dedução Natural | # Dedução Natural | ||
#* pp.41-48 de Lógica para Computação | #* pp.41-48 de Lógica para Computação | ||
+ | #* [http://www.danielclemente.com/logica/dn.en.html Introduction to natural deduction, Daniel Clemente Laboreo] | ||
+ | #* [http://membres-liglab.imag.fr/michel.levy/dn_english.php Natural Deduction] | ||
+ | #* [http://logic.tamu.edu/ The Logic Machine at Texas A&M University] | ||
+ | #* [http://pt.wikibooks.org/wiki/L%C3%B3gica:_C%C3%A1lculo_Proposicional_Cl%C3%A1ssico:_Dedu%C3%A7%C3%A3o_Natural_-_Parte_I Dedução Natural no Wikibooks] | ||
# Tablôs Analíticos | # Tablôs Analíticos | ||
#* pp. 48-56 de Lógica para Computação | #* pp. 48-56 de Lógica para Computação | ||
+ | #* [http://pt.wikibooks.org/wiki/L%C3%B3gica:_C%C3%A1lculo_Proposicional_Cl%C3%A1ssico:_Tabl%C3%B4s_sem%C3%A2nticos Tablôs Semânticos no Wikibooks] | ||
# Tablôs KE | # Tablôs KE | ||
#* [http://www.teses.usp.br/teses/disponiveis/45/45134/tde-04052007-175943/ Tese de Doutorado do professor Adolfo Neto] | #* [http://www.teses.usp.br/teses/disponiveis/45/45134/tde-04052007-175943/ Tese de Doutorado do professor Adolfo Neto] | ||
Linha 33: | Linha 119: | ||
# Resolução Proposicional | # Resolução Proposicional | ||
#* pp. 88-92 de Lógica para Computação | #* pp. 88-92 de Lógica para Computação | ||
− | # Substituição | + | #* [http://pt.wikipedia.org/wiki/Princ%C3%ADpio_da_resolu%C3%A7%C3%A3o Princípio da Resolução] |
+ | #* [http://en.wikipedia.org/wiki/J._Alan_Robinson John Alan Robinson (criador da resolução)] | ||
+ | #* [http://www.ime.usp.br/~adolfo/tmp/p163-robinson.pdf Artigo de J.A. Robinson (em PDF)] | ||
+ | # Substituição e Unificação | ||
+ | #* [http://pt.wikipedia.org/wiki/Unifica%C3%A7%C3%A3o Unificação] | ||
# Lógicas Não Clássicas | # Lógicas Não Clássicas | ||
#* [http://pt.wikibooks.org/wiki/L%C3%B3gica:_L%C3%B3gicas_N%C3%A3o-cl%C3%A1ssicas:_Introdu%C3%A7%C3%A3o Introdução] | #* [http://pt.wikibooks.org/wiki/L%C3%B3gica:_L%C3%B3gicas_N%C3%A3o-cl%C3%A1ssicas:_Introdu%C3%A7%C3%A3o Introdução] | ||
Linha 39: | Linha 129: | ||
#** [http://wwwexe.inf.ufsc.br/~arthur/publicacoes/dissertacoes/diss_Arthur.zip Dissertação de Mestrado de Arthur Buchsbaum] | #** [http://wwwexe.inf.ufsc.br/~arthur/publicacoes/dissertacoes/diss_Arthur.zip Dissertação de Mestrado de Arthur Buchsbaum] | ||
#** [ftp://logica.cle.unicamp.br/pub/e-prints/vol.5,n.1,2005-revised.pdf Logics of Formal Inconsistency] | #** [ftp://logica.cle.unicamp.br/pub/e-prints/vol.5,n.1,2005-revised.pdf Logics of Formal Inconsistency] | ||
+ | #** [http://wwwexe.inf.ufsc.br/~arthur/index.php?page=software&lang=pt Um provador automático por tablôs para os cálculos C1 e C1* de Newton da Costa, de Arthur Buchsbaum] | ||
# Ontologias | # Ontologias | ||
− | #* Procurar Ademir Freddo e | + | #* Procurar Ademir Freddo e pedir material em português |
# Provadores de Teoremas | # Provadores de Teoremas | ||
+ | #* [http://pt.wikipedia.org/wiki/Prova_autom%C3%A1tica_de_teoremas Prova automática de teoremas] | ||
+ | #* [http://en.wikipedia.org/wiki/Automated_theorem_proving Automated theorem proving] | ||
+ | #* [http://www.cin.ufpe.br/~tg/2007-2/egm2.pdf Estudo e estado da arte dos provadores automáticos de teoremas, Ewerton Guerra Marques (TCC de ex-aluno do CIN-UFPE)] | ||
# Programação em Lógica | # Programação em Lógica | ||
+ | #* Procurar no livro "Lógica para Ciência da Computação" | ||
+ | #* Procurar "prolog" no Google | ||
+ | #* [http://pt.wikipedia.org/wiki/Prolog Prolog] | ||
# Uma linguagem de Especificação | # Uma linguagem de Especificação | ||
+ | #* Escolher entre Z, VDM-SL e Alloy (ou propor outra) | ||
+ | #** Z | ||
+ | #*** [http://pt.wikipedia.org/wiki/Z_notation Z na Wikipedia] | ||
+ | #*** [http://formalmethods.wikia.com/wiki/Z_notation Página Wiki sobre Z] | ||
+ | #*** [http://spivey.oriel.ox.ac.uk/mike/zrm/zrm.pdf The Z Notation, J. M. Spivey] | ||
+ | #*** [http://staff.washington.edu/jon/z/z-examples.html Z Notation Examples] | ||
+ | #*** [http://www.teses.usp.br/teses/disponiveis/45/45134/tde-02112008-224245/ Geração parcial de código Java a partir de especificações formais Z, Alvaro Heiji Miyazawa] | ||
+ | #*** [http://www.usingz.com/text/online/index.html Livro "Using Z"] | ||
+ | #**** [http://www.usingz.com/text/online/page-217.html Exemplo: A File System] | ||
+ | #*** [http://tug.ctan.org/cgi-bin/ctanPackageInformation.py?id=objectz ObjectZ - Latex macros for typesetting Object Z] | ||
+ | #** [http://ze.ic.unicamp.br/WWW/Disciplinas/INF309/ Página de disciplina sobre Métodos Formais] | ||
+ | #*** [http://zeves.blogspot.com/2008_06_01_archive.html Blog com alguns links] | ||
+ | #** VDM-SL | ||
+ | #*** [http://www.ic.unicamp.br/~eliane/Cursos/MO409/artigos/artigo-vdm.ps Modelagem e Especificação de Sistemas usando VDM: um Survey, Adilson Luiz Bonifácio e Rodrigo Bonacin] | ||
+ | #*** [http://www.vdmportal.org/twiki/bin/view/Main/VDMSLexamples Vários exemplos de VDM-SL (em inglês - diversos autores)] | ||
+ | #*** [http://wiki.di.uminho.pt/twiki/bin/view/Education/Archive/EDFS Especificação e Desenvolvimento Formal de Software (contém vários links)] | ||
+ | #*** [http://en.wikipedia.org/wiki/Vienna_Development_Method VDM na Wikipedia] | ||
+ | #*** [http://www.ic.unicamp.br/~eliane/Cursos/MO409/Curso2003/Apresentacoes/VDM.ppt Slides sobre VDM, Cibele Brunetto - Unicamp (contém Bibliografia!)] | ||
+ | #*** [http://atterer.net/uni/sep/ Automatic Test Data Generation From VDM-SL Specifications] | ||
+ | #*** [http://glasnost.itcarlow.ie/~meudecc/research/thesis/thesis.zip Tese de Doutorado sobre VDM] | ||
+ | #*** [http://wiki.di.uminho.pt/twiki/bin/view/Education/Archive/EDFS Especificação e Desenvolvimento Formal de Software] | ||
# Um provador de teoremas | # Um provador de teoremas | ||
+ | #* Escolher entre Otter, Isabelle, Lotrec, zChaff ou KEMS (ou propor outro) | ||
# Ontologias e Web Semântica (com lógicas de descrição) | # Ontologias e Web Semântica (com lógicas de descrição) | ||
#* [http://www.eci.ufmg.br/mba/onto_frames/index.htm Tutorial básico do Protege] | #* [http://www.eci.ufmg.br/mba/onto_frames/index.htm Tutorial básico do Protege] | ||
+ | |||
+ | == Regras == | ||
+ | |||
+ | === Forma de entrega === | ||
+ | |||
+ | Os arquivos referentes aos itens abaixo deverão ser entregues/enviados pelo [http://ead.dainf.ct.utfpr.edu.br/course/view.php?id=21 sistema de EAD do DAINF]. | ||
+ | |||
+ | === Apresentação === | ||
+ | |||
+ | Cada apresentação consistirá de: | ||
+ | # uma equipe (a equipe apresentadora) apresentando o assunto (usando ''slides'', quadro e outros recursos que achar conveniente) | ||
+ | #* esta apresentação deverá durar de 20 a 30 minutos | ||
+ | #* todos os integrantes da equipe devem participar desta apresentação | ||
+ | #* todos os integrantes da equipe devem conhecer TODO o assunto | ||
+ | # Depois disso, uma equipe (a equipe debatedora) deverá fazer perguntas para testar os conhecimentos da equipe apresentadora. Durante este debate (com duração de até 15 minutos), ambas as equipes serão avaliadas. | ||
+ | |||
+ | === Parte Escrita === | ||
+ | |||
+ | * Tamanho: entre 5 e 10 páginas | ||
+ | * Usar o [http://www.sbc.org.br/index.php?language=1&subject=60&content=downloads&id=286 modelo para publicação de artigos da SBC] mas, para as referências, seguir o padrão ABNT que pode ser encontrado nas [http://www.utfpr.edu.br/documentos/normas_trabalhos_utfpr.pdf NORMAS PARA ELABORAÇÃO DE TRABALHOS ACADÊMICOS da UTFPR] | ||
+ | * A parte escrita é preparada exclusivamente pela equipe apresentadora e deverá ser entregue uma semana antes da apresentação para o professor e para a equipe debatedora. | ||
+ | |||
+ | === Resolução dos Exercícios === | ||
+ | |||
+ | * Para aquelas equipes cujo assunto está no livro "Lógica para Computação", será exigida também a entrega (em formato digital) da resolução completa dos exercícios do livro referentes ao assunto. | ||
+ | |||
+ | === Entrada na Wiki do DAINF === | ||
+ | |||
+ | A partir da parte escrita, a equipe deverá preparar uma entrada (mini-artigo) que será publicada na Wiki do DAINF. | ||
+ | |||
+ | === ''Slides'' da Apresentação === | ||
+ | |||
+ | Os ''slides'' da apresentação deverão ser entregues com uma semana de antecedência. | ||
+ | |||
+ | Observações importantes: | ||
+ | * procure começar sua apresentação com um exemplo, que deverá ser retomado após a apresentação das bases formais; | ||
+ | * os slides devem ser numerados. | ||
+ | |||
+ | == Critérios de Avaliação == | ||
+ | |||
+ | # Apresentação '''(peso 2)''' | ||
+ | #* Domínio do conteúdo | ||
+ | #* Capacidade de expressão | ||
+ | # Parte escrita '''(peso 3)''' | ||
+ | #* Conteúdo | ||
+ | #* Qualidade do texto | ||
+ | #* Originalidade | ||
+ | #* Concordância com as normas ABNT | ||
+ | # Resolução dos exercícios '''(peso 1)''' | ||
+ | #* Correção das respostas | ||
+ | # Entrada no wiki do DAINF '''(peso 1)''' | ||
+ | #* Conteúdo | ||
+ | #* Qualidade do texto | ||
+ | #* Originalidade | ||
+ | #* Concordância com as normas Wiki | ||
+ | # Slides da apresentação '''(peso 1)''' | ||
+ | #* Legibilidade | ||
+ | #* Citação de referências | ||
+ | #** Todo slide que contiver material (figura, texto, etc) que não tenha sido desenvolvido pela equipe, deverá conter, na parte inferior da página, em fonte pequena, a referência: "Fonte: (REFERÊNCIA ESTILO ABNT)." Por exemplo, se alguém usar a foto de Hal Abelson obtida da Wikipedia, deverá citar da seguinte forma: "Fonte: WIKIPEDIA. '''Hal Abelson.''' Disponível em:<http://en.wikipedia.org/wiki/Hal_Abelson>. Acesso em: 23 mar. 2009." | ||
+ | # Participação no debate '''(peso 2)''': cada participante de equipe (debatedora ou apresentadora) será avaliado durante o debate de acordo com os seguintes critérios: | ||
+ | #* participação ativa no debate | ||
+ | #* qualidade e pertinência das perguntas feitas | ||
+ | #* correção das respostas dadas |
Edição atual tal como 16h45min de 26 de junho de 2009
Informações sobre o oferecimento da disciplina Lógica para Computação em 2009.1.
Tabela de conteúdo |
Projeto Integrado - Turma S73 - 2009.1
Projeto Final - Turma S71 - 2009.1
Assuntos e Equipes das Apresentações
Engenharia de Computação (S71)
- Axiomatização: Vinícius, Daniel e André
- 24/03/2009
- Equipe debatedora: 12
- Dedução Natural: Alexandre, Liège e Danilo
- 24/03/2009
- Equipe debatedora: 11
- Tablôs Analíticos: Rebeca, Líria e Cristiane
- 25/03/2009
- Equipe debatedora: 10
- Tablôs KE: Lucas, Demétrius e João
- 25/03/2009
- Equipe debatedora: 9
- Formas Normais: Kelvin, Dalton e Jorge
- 31/03/2009
- Equipe debatedora: 8
- Resolução Proposicional: Henrique P., Cibele e Amanda
- 01/04/2009
- Equipe debatedora: 7
- Substituição e Unificação: Felipe Lisboa, Victor Perales e Bruno Bellucci
- 15/04/2009
- Equipe debatedora: 1
- Lógicas Não Clássicas: Eduardo Bonet, Tiago e Jean
- 28/04/2009
- Equipe debatedora: 14
- Ontologias: Márcio, Cláudio, Henrique Rein.
- 05/05/2009
- Equipe debatedora: 13
- Programação em Lógica: Augusto, Guilherme, Marlon Bill
- 06/05/2009
- Equipe debatedora: 5
- Z, uma linguagem de Especificação: Suleiman, Rafael, Julio, Luiz
- 12/05/2009
- Equipe debatedora: 4
- Ontologias e Web Semântica (com lógicas de descrição): Marcos, André, Maurício
- 13/05/2009
- Equipe debatedora: 3
- VDM-SL, uma linguagem de especificação: Fabio César, Eduardo Rachid e Cleverson
- 19/05/2009
- Equipe debatedora: 6
- Provador de teorema - Otter: André Luiz, Gionatta e Pedro.
- 20/05/2009
- Equipe debatedora: 2
Bacharelado em Sistemas de Informação (S73)
- Axiomatização: Lucas Campos Silva, Marcelo Butzke Leopoldino, Isaac Toyoshi Takiguchi Jr.
- 25/03/2009
- Equipe debatedora: 14
- Dedução Natural: Rubens Carlos Meggetto Junior, Estevan Frederico Pasquetta Jantsk, Thomaz Teodorovicz
- 25/03/2009
- Equipe debatedora: 13
- Tablôs Analíticos: Daniel Felipe Warkentin, Raul Vitor Tessaro Esteves
- 01/04/2009
- Equipe debatedora: 12
- Tablôs KE: Cristiano De Oliveira Viana Correia, Jonatas Da Luz, Luan Nestor Vageti Aruquipa
- 03/04/2009
- Equipe debatedora: 11
- Formas Normais: Emerson Shigueo Sugimoto, Rodrigo Cirino De Andrade, Vagner Vengue
- 22/04/2009
- Equipe debatedora: 10
- Resolução Proposicional: Ana Paula Ferreira, Fernando Bozza, Vanessa Maria Da Silva
- 29/04/2009
- Equipe debatedora: 9
- Substituição e Unificação: Bruno Milczewski, Mario Sergio Esperanca Silva, Thiago Vinicius Pereira
- 06/05/2009
- Equipe debatedora: 1
- Lógicas Não Clássicas: Andressa Caroline Portes Da Cunha, Melina Deraldo Dos Santos, Thays Boiko
- 08/05/2009
- Equipe debatedora: 2
- Ontologias: Fernando Hiroshi Suemitsu, Bruno Guilherme Andretta De Miranda, Matheus Alves De Souza
- 13/05/2009
- Equipe debatedora: 3
- Provadores de Teoremas - Visão geral: Andrei Magaievski, Andre Luiz De Lacerda, Ricardo Trizzolini Piekarski
- 15/05/2009
- Equipe debatedora: 4
- Programação em Lógica: Andre Hoeldtke Castro, Rafael Oliveira Tavares Pinto, Vinicius Andreatta
- 20/05/2009
- Equipe debatedora: 8
- A linguagem de especificação Z: Bruna Pereira Segan, Leticia Ueda, Kelly Cristina Schultz
- 22/05/2009
- Equipe debatedora: 7
- Um provador de teoremas - KEMS: Eduardo Carvalho Zanello, Gregorio Ivanchechen De Mattos, Pablo Kravicz, Ana Cristina Da Silva
- 27/05/2009
- Equipe debatedora: 6 e 5
Material para os Trabalhos
- Axiomatização
- pp.33-41 de Lógica para Computação
- Dedução Natural
- pp.41-48 de Lógica para Computação
- Introduction to natural deduction, Daniel Clemente Laboreo
- Natural Deduction
- The Logic Machine at Texas A&M University
- Dedução Natural no Wikibooks
- Tablôs Analíticos
- pp. 48-56 de Lógica para Computação
- Tablôs Semânticos no Wikibooks
- Tablôs KE
- Formas Normais
- pp. 77-88 de Lógica para Computação
- Resolução Proposicional
- pp. 88-92 de Lógica para Computação
- Princípio da Resolução
- John Alan Robinson (criador da resolução)
- Artigo de J.A. Robinson (em PDF)
- Substituição e Unificação
- Lógicas Não Clássicas
- Introdução
- A lógica paraconsistente <math>C_1</math>, de Newton da Costa
- Ontologias
- Procurar Ademir Freddo e pedir material em português
- Provadores de Teoremas
- Programação em Lógica
- Procurar no livro "Lógica para Ciência da Computação"
- Procurar "prolog" no Google
- Prolog
- Uma linguagem de Especificação
- Escolher entre Z, VDM-SL e Alloy (ou propor outra)
- Z
- Página de disciplina sobre Métodos Formais
- VDM-SL
- Modelagem e Especificação de Sistemas usando VDM: um Survey, Adilson Luiz Bonifácio e Rodrigo Bonacin
- Vários exemplos de VDM-SL (em inglês - diversos autores)
- Especificação e Desenvolvimento Formal de Software (contém vários links)
- VDM na Wikipedia
- Slides sobre VDM, Cibele Brunetto - Unicamp (contém Bibliografia!)
- Automatic Test Data Generation From VDM-SL Specifications
- Tese de Doutorado sobre VDM
- Especificação e Desenvolvimento Formal de Software
- Escolher entre Z, VDM-SL e Alloy (ou propor outra)
- Um provador de teoremas
- Escolher entre Otter, Isabelle, Lotrec, zChaff ou KEMS (ou propor outro)
- Ontologias e Web Semântica (com lógicas de descrição)
Regras
Forma de entrega
Os arquivos referentes aos itens abaixo deverão ser entregues/enviados pelo sistema de EAD do DAINF.
Apresentação
Cada apresentação consistirá de:
- uma equipe (a equipe apresentadora) apresentando o assunto (usando slides, quadro e outros recursos que achar conveniente)
- esta apresentação deverá durar de 20 a 30 minutos
- todos os integrantes da equipe devem participar desta apresentação
- todos os integrantes da equipe devem conhecer TODO o assunto
- Depois disso, uma equipe (a equipe debatedora) deverá fazer perguntas para testar os conhecimentos da equipe apresentadora. Durante este debate (com duração de até 15 minutos), ambas as equipes serão avaliadas.
Parte Escrita
- Tamanho: entre 5 e 10 páginas
- Usar o modelo para publicação de artigos da SBC mas, para as referências, seguir o padrão ABNT que pode ser encontrado nas NORMAS PARA ELABORAÇÃO DE TRABALHOS ACADÊMICOS da UTFPR
- A parte escrita é preparada exclusivamente pela equipe apresentadora e deverá ser entregue uma semana antes da apresentação para o professor e para a equipe debatedora.
Resolução dos Exercícios
- Para aquelas equipes cujo assunto está no livro "Lógica para Computação", será exigida também a entrega (em formato digital) da resolução completa dos exercícios do livro referentes ao assunto.
Entrada na Wiki do DAINF
A partir da parte escrita, a equipe deverá preparar uma entrada (mini-artigo) que será publicada na Wiki do DAINF.
Slides da Apresentação
Os slides da apresentação deverão ser entregues com uma semana de antecedência.
Observações importantes:
- procure começar sua apresentação com um exemplo, que deverá ser retomado após a apresentação das bases formais;
- os slides devem ser numerados.
Critérios de Avaliação
- Apresentação (peso 2)
- Domínio do conteúdo
- Capacidade de expressão
- Parte escrita (peso 3)
- Conteúdo
- Qualidade do texto
- Originalidade
- Concordância com as normas ABNT
- Resolução dos exercícios (peso 1)
- Correção das respostas
- Entrada no wiki do DAINF (peso 1)
- Conteúdo
- Qualidade do texto
- Originalidade
- Concordância com as normas Wiki
- Slides da apresentação (peso 1)
- Legibilidade
- Citação de referências
- Todo slide que contiver material (figura, texto, etc) que não tenha sido desenvolvido pela equipe, deverá conter, na parte inferior da página, em fonte pequena, a referência: "Fonte: (REFERÊNCIA ESTILO ABNT)." Por exemplo, se alguém usar a foto de Hal Abelson obtida da Wikipedia, deverá citar da seguinte forma: "Fonte: WIKIPEDIA. Hal Abelson. Disponível em:<http://en.wikipedia.org/wiki/Hal_Abelson>. Acesso em: 23 mar. 2009."
- Participação no debate (peso 2): cada participante de equipe (debatedora ou apresentadora) será avaliado durante o debate de acordo com os seguintes critérios:
- participação ativa no debate
- qualidade e pertinência das perguntas feitas
- correção das respostas dadas