Wiki DAINF - Contribuições do usuário [pt-br]

Formas Normais: Emerson Shigueo Sugimoto, Rodrigo Cirino De Andrade, Vagner Vengue

2009-04-21T06:45:39Z

Vagnervengue: Nova página: Referem-se as fórmulas da lógica proposicional que se encontram definidas apenas pelos conectivos: Λ(conjunção), V(disjunção) e ¬(negação). Podendo estar na Forma Normal Conj...

Referem-se as fórmulas da lógica proposicional que se encontram definidas apenas pelos conectivos: Λ(conjunção), V(disjunção) e ¬(negação). Podendo estar na Forma Normal Conjuntiva(onde o conectivo princial é a conjunção) ou Forma Normal Disjuntiva(onde o conectivo principal é a disjunção).

== FORMAS NORMAIS ==

As fórmulas normais são as fórmulas da lógica proposicional apresentadas num formato definido, ou seja, são fórmulas que são moldadas para serem exibidas em um formato definido. Sendo duas as principais formas normais: '''FNC''' – forma normal conjuntiva e a '''FND''' – forma normal disjuntiva, exemplos:

H = (¬P Λ Q) V (¬R Λ ¬Q Λ P) V (P Λ S) – forma normal disjuntiva (V).

G = (¬P V Q) Λ (¬R V ¬Q V P) Λ (P V S) – forma normal conjuntiva (Λ).

== FNC ou FORMA CLAUSAL ==

A FNC (forma normal conjuntiva) também é chamada de forma clausal. O elemento básico da FNC é o '''literal''', que é uma fórmula atômica, por exemplo em p Λ q Λ r, os literais são: p, q e r.
 Uma '''cláusula''' é a disjunção de literais: L1 V L2 V ... L.
 Exemplos:
 (¬p V Y)
 (¬p V Z)
 (¬Y V ¬Z V p)

Uma fórmula é a conjunção de cláusulas, exemplo:
 (¬p V Y) Λ (¬p V Z) Λ (¬Y V ¬Z V p)

Quando em uma fórmula a negação só pode estar aplicada aos átomos, ela é dita Forma Normal de Negação – '''FNN''', isto significa que não pode haver uma negação de uma cláusula, a negação deve ser empurrada para os átomos, conforme a lei De Morgan.

=== ALGORITIMO 1 - TRANSFORMAÇÃO DA FNC SEM NOVOS ÁTOMOS ===

 '''Entrada''': Uma fórmula B.
 '''Saída''': Uma fórmula A na FNC, B º A .
 1: '''para''' todas as subfórmulas X, Y, Z de B '''faça'''
 2: Redefinir “→” em termos de “V” e “¬”:
 (X → Y) <=> (¬X V Y)
 3: Empurrar as negações para o interior por meio das leis De Morgan :
 ¬ (X V Y) <=> ¬X Λ ¬Y
 ¬ (X Λ Y) <=> ¬X V ¬Y
 4: Eliminação da dupla negação:
 ¬¬ X X
 5: Distributividade de V sobre Λ:
 X V (Y Λ Z) <=> (X V Y) Λ (X V Z)
 6: '''fim para'''
 7: A fórmula A é obtida quando não há mais substituições possíveis.

Apesar de gerar uma fórmula FNC, ele pode gerar fórmulas exponencialmente maiores que a fórmula de entrada. O problema esta no passo 5 da distributividade, que causa a duplicação da subfórmula X, que por sua vez pode ser no formato (X1 Λ X2), que poderá gerar uma nova duplicação.

=== ALGORITIMO 2 - TRANSFORMAÇÃO LINEAR PARA FNC COM ADIÇÃO DE NOVOS ÁTOMOS ===

 '''Entrada''': Uma fórmula B.
 '''Saída''': Uma fórmula A na FNC, B º A.
 1: para todas as subfórmulas X, Y, Z de B faça
 2: Redefinir “ → ” em termos de “V” e “¬”:
 (X → Y) <=> (¬X V Y)
 3: Empurrar as negações para o interior por meio das leis De Morgan:
 ¬ (X V Y) <=> ¬X Λ ¬Y
 ¬ (X Λ Y) <=> ¬X V ¬Y
 4: Eliminação da dupla negação:
 ¬¬ X <=> X
 5: Inserção de novo átomo p:
 X V (Y Λ Z) <=> (X V p) Λ (¬p V Y) Λ (¬p V Z) Λ (¬Y V ¬Z V p)
 6: '''fim para'''
 7: A fórmula A é obtida quando não há mais substituições possíveis.

 No ALGORITMO 2, foi introduzido um novo símbolo atômico p, de forma que p ↔ (Y Λ Z), ou seja, p têm a mesma valoração de (Y Λ Z), desmembrando ↔ em dois:
 (p → (Y Λ Z)) Λ (Y Λ Z → p).
 Eliminando “→”, aplicando a redefinição de “→” em termos de “V” e “¬”(X → Y) <=> (¬X V Y):
 (¬p V (Y Λ Z)) Λ (¬(Y Λ Z) V p).
 Em seguida por meio das leis De Morgan, empurramos a negação adentro (convertendo V em Λ):
 (¬p V (Y Λ Z)) Λ (¬Y V ¬Z V p)
 O segundo elemento já esta já está no formato clausal, no primeiro elemento não há
dupla negação, e será aplicada a distribuição de V sobre Λ, obtendo-se:
 (¬p V Y) Λ (¬p V Z) Λ (¬Y V ¬Z V p)
 A vantagem das fórmulas clausais está na representação e solução de problemas envolvendo fórmulas proposicionais, pois para se satisfazer uma fórmula do formato clausal, basta satisfazer um literal em cada uma das suas cláusulas, e para falsificar uma fórmula no formato clausal, basta falsificar todos os literais de uma única cláusula, ou seja, falsificar uma cláusula.

== CLÁUSULAS DE HORN ==

As Cláusulas de Horn são cláusulas (conjunto de literais) na forma disjuntiva com no máximo um literal positivo, exemplo:
 ¬ p V ¬ q V. . . V r
 Estas cláusulas podem ser divididas em três formas: Fatos, Regras e Consulta ou Restrições.
 '''Fatos''' são cláusulas com apenas um literal positivo e são usadas para afirmar que um literal é válido, por exemplo p, q e r.
 '''Regras''' são cláusulas com exatamente um literal positivo, exemplo:
 (¬ p V ¬ q V r)
 Ou, de acordo com as equivalências notáveis:
 ¬ (p Λ . . . Λ q) V r, (lei de De Morgan).
 (p Λ . . . Λ q) → r (definição de → em termos de V e ¬)
 Na qual, p Λ . . . Λ q é chamado de corpo da regra e r é chamado de cabeça da regra.
 '''Consultas ou Restrições''' são cláusulas com apenas literais negativos, exemplo:
 (¬ p V ¬ q V ¬ r V ¬s)

=== FÓRMULAS DE HORN ===

 Fórmulas de Horn são um conjunto de cláusulas de Horn na forma normal conjuntiva, exemplo:
 (¬ p V q) Λ (r V ¬ s) Λ (a V ¬a) Λ (a V ¬b)
 Uma das propriedades das cláusulas de Horn é a respeito do princípio da resolução: duas cláusulas de Horn regras inferem outra cláusula de Horn e uma cláusula do tipo consulta ou restrição com uma cláusula regra infere uma cláusula também do tipo consulta ou restrição.

 As cláusulas de Horn receberam este nome em homenagem ao lógico matemático Alfred Horn, que em 1951 publicou no jornal Journal of Symbolic Logic o artigo “On sentences which are true of direct unions of algebras”. Alfred Horn foi o primeiro a chamar a atenção para estes tipos de cláusulas, que hoje, através de suas propriedades, com o princípio da resolução dão base à programação lógica e a linguagem de programação Prolog.

== FORMA NORMAL DISJUNTIVA (FND) ==

Na lógica booleana, uma forma normal disjuntiva ('''FND''') é uma normalização de uma fórmula lógica no qual temos uma disjunção de conjunções de literais. Também chamada cláusula dual.
Uma conjunção de literais disjuntivos tem a forma de:

 A1 Λ A2 Λ... Λ An

Podemos encontrar na forma de polinômios, em que a conjunção é representada pela multiplicação (*), e a disjunção pela adição (+) e a negação por uma barra sobre o átomo (Ū) por exemplo a fórmula ( ¬p1Λ p2 ) V ( p1Λ¬p2 ) pode ser expresso em notação polinomial da seguinte forma:

 Ū1 U2 + Ū1 U2

Toda fórmula proposicional pode ser transformada em uma forma do tipo disjuntiva para isso podemos usar meios como a lei da Dupla Negação, as leis de De Morgan e a distributividade de átomos.

Uma fórmula disjuntiva só é verdadeira quando ao menos uma de suas subfórmulas é verdadeira, exemplos:
 v (P) = 1 <=> v (P V Q) = 1
 v (Q) = 1 <=> v (P V Q) = 1
 Repare que a disjunção também é comutativa, ou seja que pode haver troca na ordem dos operadores sem perda do resultado.
 Assim, se P significa "Fulano estuda filosofia" e Q significa "Fulano estuda matemática", P V Q pode ser interpretada como "Fulano estuda filosofia ou matemática"; o que só é falso se nem P nem Q forem verdadeiras.
 Com a disjunção é preciso tomar muito cuidado tanto na interpretação de fórmulas quanto na formalização de proposições, pois na linguagem natural muitas vezes os disjuntos são excludentes. Por exemplo: "Uma moeda ao ser lançada resulta em cara ou coroa".
Veja essas proposições:

 Proposição I - «Gosta de lógica e/ou gosta de método» ( L V M )
 Proposição E - «Ou gosta de lógica ou gosta de métodos» ( L VV M )

Ambas proposições são resultado da disjunção das duas proposições simples:
 «Gosta de Lógica» - proposição L
 «Gosta de Métodos» - proposição M

A proposição I diz que é possível gostar apenas de lógica ou de métodos, mas também se pode gostar das duas disciplinas.

A proposição E diz que se gosta de lógica, então não gosta de métodos. Mas, se for o caso que goste de métodos, então não gosta de lógica. As duas proposições M e L não são compatíveis uma com a outra; isto é, a verdade de uma significa a falsidade da outra.

Logo sabemos que há:

 A proposição I é a que podemos chamar de disjunção inclusiva (V).
 A proposição E é a que podemos chamar de disjunção exclusiva (VV)

Finalizando (A VV B) só é V se, e somente se, A e B têm valores-verdade diferentes.
 Exemplos de forma normal disjuntiva:
 A V B
 A
 (A Λ B) V C
 (A Λ ¬B Λ ¬C) V (¬D Λ E Λ F)
 (A Λ B Λ ¬C) V (B Λ ¬D Λ ¬E) V (A Λ F)

Todavia, as seguintes fórmulas não estão na FND:
 ¬(A V B) — NÃO é o operador mais extremo
 A V (B Λ (C V D)) — um OU está aninhado com um E
 De acordo com o que vemos nas leis de De Morgan, numa expressão da forma conjuntiva temos:
 ¬(P Λ Q) <=> (¬P V ¬Q)

Podemos aferir o contrário pela bi-implicação (↔), obtendo uma formula disjuntiva:
 (¬P V ¬Q) <=> ¬(P Λ Q)

=== ALGORITIMO 3 - TRANSFORMAÇÃO NA FND SEM ADIÇÃO DE NOVOS ÁTOMOS ===

 '''Entrada''': Uma fórmula B.
 '''Saída''': Uma fórmula A na FND, B ≡ A.
 1: '''para''' todas as subfórmulas X, Y, Z de B faça
 2: Redefinir “→” em termos de “V” e “¬”:
 (X → Y) <=> (¬X V Y)
 3: Empurrar as negações para o interior por meio das leis De Morgan:
 ¬ (X V Y) <=> ¬X Λ ¬Y
 ¬ (X Λ Y) <=> ¬X V ¬Y
 4: Eliminação da dupla negação:
 ¬¬ X X
 5: distributividade de Λ sobre V :
 X Λ ( Y V Z ) <=> ( X Λ Y ) V ( X Λ Z)
 6: '''fim para'''
 7: A fórmula A é obtida quando não há mais substituições possíveis.
 Repare no conectivo de disjunção V:
 X Λ ( Y V Z ) <=> ( X Λ Y ) V ( X Λ Z)

 Aqui vemos o mesmo problema na FNC, que é o aumento proporcional da fórmula, mesmo sem adicionarmos novos átomos, ela aumenta exponencialmente com a distributividade dos átomos em novas cláusulas fora isso difere da FNC na mudança do conectivo, como vemos na regra número 5.

== REFERÊNCIAS ==

*DIAS, Carlos Magno Corrêa. Lógica Matemática: Introdução ao Cálculo Proposicional. Curitiba, C. M. Corrêa Dias, 1999.

*SOUZA, João Nunes de. Lógica para ciência da Computação: Fundamentos de linguagem, semântica e sistemas de dedução. Rio de Janeiro: Campus, 2002.

*SILVA, Flávio Soares Corrêa da; FINGER, Marcelo; MELO, Ana Cristina Vieira de. Lógica para computação. São Paulo: Editora Thompson, 2006. 234 p. ISBN 85-221-0517-0

*Augustus Morgan matemático e lógico britânico. Disponível em: <http://www.colegiosaofrancisco.com.br/alfa/augustus-de-morgan/augustus-de-morgan.php>[http://www.colegiosaofrancisco.com.br/alfa/augustus-de-morgan/augustus-de-morgan.php] Acesso em 12.abr.2009.

*Formas normais: Disponível em: <http://polo1.marilia.unesp.br/Home/Instituicao/Docentes/RicardoTassinari/LI08.pdf>[http://polo1.marilia.unesp.br/Home/Instituicao/Docentes/RicardoTassinari/LI08.pdf] Acesso em 12.abr.2009.

*WIKIPÉDIA. Enciclopédia multilíngüe on-line livre. Teoremas De Morgan.
Disponível em: <http://pt.wikipedia.org/wiki/Leis_De_Morgan>[http://pt.wikipedia.org/wiki/Leis_De_Morgan] Acesso em 28.mar.2009.

*WIKIPÉDIA. Enciclopédia multilíngüe on-line livre. Teoremas De Morgan.
Disponível em: <http://pt.wikipedia.org/wiki/Cl%C3%A1usula_de_Horn>[http://pt.wikipedia.org/wiki/Cl%C3%A1usula_de_Horn] Acesso em 04.abr.2009.

*WIKIPÉDIA. Enciclopédia multilíngüe on-line livre. Teoremas De Morgan.
Disponível em: <http://pt.wikipedia.org/wiki/Cl%C3%A1usula_de_Horn>[http://pt.wikipedia.org/wiki/Cl%C3%A1usula_de_Horn] Acesso em 04.abr.2009.

*WIKIPÉDIA. Enciclopédia multilíngüe on-line livre. Distributividade. Disponível em: <http://pt.wikipedia.org/wiki/Distributividade>[http://pt.wikipedia.org/wiki/Distributividade] Acesso em 12.abr.2009.

*WIKIPÉDIA. Enciclopédia multilíngüe on-line livre. lei da dupla negação. Disponível em: <http://pt.wikipedia.org/wiki/Dupla_nega%C3%A7%C3%A3o>[http://pt.wikipedia.org/wiki/Dupla_nega%C3%A7%C3%A3o] Acesso em 12.abr.2009.

*WIKIPÉDIA. Enciclopédia multilíngüe on-line livre. Formal normal disjuntiva. Disponível em: [http://pt.wikipedia.org/wiki/Forma_normal_disjuntiva]<http://pt.wikipedia.org/wiki/Forma_normal_disjuntiva> Acesso em 12.abr.2009.

Aqui

2009-04-21T04:00:07Z

Vagnervengue: Nova página: ===Formas Normais===

===Formas Normais===

Lógica para Computação - Turmas S71 e S73 - 2009.1

2009-04-21T03:58:30Z

Vagnervengue: /* Bacharelado em Sistemas de Informação (S73) */

Informações sobre o oferecimento da disciplina [[Lógica para Computação]] em 2009.1.

== Assuntos e Equipes ==

=== 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
#* 22/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, 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
#* 24/04/2009
#* Equipe debatedora: 9
# Substituição e Unificação: Bruno Milczewski, Mario Sergio Esperanca Silva, Thiago Vinicius Pereira
#* 29/04/2009
#* Equipe debatedora: 1
# Lógicas Não Clássicas: Andressa Caroline Portes Da Cunha, Melina Deraldo Dos Santos, Thays Boiko
#* 06/05/2009
#* Equipe debatedora: 2
# Ontologias: Fernando Hiroshi Suemitsu, Bruno Guilherme Andretta De Miranda, Matheus Alves De Souza
#* 08/05/2009
#* Equipe debatedora: 3
# Provadores de Teoremas: Andrei Magaievski, Andre Luiz De Lacerda, Ricardo Trizzolini Piekarski
#* 13/05/2009
#* Equipe debatedora: 4
# Programação em Lógica: Andre Hoeldtke Castro, Rafael Oliveira Tavares Pinto, Vinicius Andreatta
#* 15/05/2009
#* Equipe debatedora: 8
# A linguagem de especificação Z: Bruna Pereira Segan, Leticia Ueda, Kelly Cristina Schultz
#* 20/05/2009
#* Equipe debatedora: 7
# Um provador de teoremas: Eduardo Carvalho Zanello, Gregorio Ivanchechen De Mattos, Pablo Kravicz, Ana Cristina Da Silva
#* 22/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
#* [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
#* 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
#* [http://www.teses.usp.br/teses/disponiveis/45/45134/tde-04052007-175943/ Tese de Doutorado do professor Adolfo Neto]
# Formas Normais
#* pp. 77-88 de Lógica para Computação
# Resolução Proposicional
#* pp. 88-92 de Lógica para Computaçã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
#* [http://pt.wikibooks.org/wiki/L%C3%B3gica:_L%C3%B3gicas_N%C3%A3o-cl%C3%A1ssicas:_Introdu%C3%A7%C3%A3o Introdução]
#* A lógica paraconsistente <math>C_1</math>, de Newton da Costa
#** [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]
#** [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
#* Procurar Ademir Freddo e pedir material em português
# 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]
# 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
#* Escolher entre Z, VDM e Alloy (ou propor outra)
#** Z
#*** [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]
#** VDM
#*** [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://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
#* Escolher entre Otter, Isabelle, Lotrec, zChaff ou KEMS (ou propor outro)
# 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]

== 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

Voluntários ERI 2009

2009-04-08T14:27:23Z

Vagnervengue:

= Voluntários =

Peço aos alunos que se dispuserem a ajudar na organização do ERI 2009 (ainda sem data definida) que coloquem seus nomes na lista abaixo.

A ajuda poderá acontecer de várias formas, desde ficar responsável por não deixar faltar água mineral aos palestrantes, preparar pastas para os participantes, até ajudar a criar e manter um site para o evento, entre outras coisas.

Dependo desta lista de voluntários (no mínimo 30) para enviar à regional Paraná da SBC um pedido (que pode não ser aceito) para que a ERI aconteça aqui na UTFPR.
Se, por algum motivo, o aluno que colocar o nome na lista não puder participar da organização, não há qualquer problema.

Em caso de dúvidas, entrem em contato comigo, [[Adolfo Neto]]

== Alunos ==

{| class="wikitable sortable" align="left"
|+ Alunos voluntários para ERI 2009
|-
! align="left" |Nome do aluno
! align="left" |Curso
! align="left" |Período que está cursando
|-
| Aline Macohin
| TSI
| 5
|-
| Ricardo Trizzolini Piekarski
| BSI
| 1
|-
| Emilio Seidel Fernandes
| TDSD
| 6
|-
| Marlos Otávio Corrêa da Silva
| TDSD
| 6
|-
| Cleverson Luiz Ferreira
| EC
| 1
|-
| Rafael Apetz Bressan
| TSI
| 3
|-
| Ewerton Julian Rubio
| TSI
| 3
|-
| Diogo Vinicius França
| TSI
| 3
|-
| Daiane Assen Chales
| TSI
| 4
|-
| Marcelo Butzke Leopoldino
| BSI
| 1
|-
| Rodrigo Cirino de Andrade
| BSI
| 1
|-
| Cristiano de Oliveira Viana Correia
| BSI
| 1
|-
| Cintia Elisa Effting
| TSI
| 2
|-
| Daniel Leal Valente
| TSI
| 3
|-
| Tiago Sereneski Rocha
| EC
| 1
|-
| Leandro Ferreira Heroso
| EC
| 2
|-
| Jean Quevedo
| EC
| 1
|-
| Vagner Vengue
| BSI
| 1
|-
|}