Re: [Logica-l] Lógica e Acessibilidade
2012/4/13 Elias Gabriel Amaral da Silva : > 2012/4/13 Aracele Garcia de Oliveira : > Mas o aluno raciocinar, utilizando regras do sistema >> dedutivo, por exemplo, para este aluno mesmo criar a prova, aí é que está o >> "problema". > > > Pois é o que estou falando, o ProofWeb permite isto! Deixa eu te dar outro exemplo, um exercício que eu resolvi, considerado "fácil", que foi provar (C /\ C) -> A, C \/ (C /\ A) |- (( B <-> B ) -> C) /\ (B -> A) Eu tirei um printscreen da visualização da prova, usando tanto diagramas de Fitch quanto árvores. A visualização vai aparecendo à medida que eu digito a prova http://i.imgur.com/0zsoo.png http://i.imgur.com/26tRa.png À medida que a prova vai evoluindo, naquela janela que aparece "Proof completed" iria aparecer as hipóteses que você ganhou por alguma regra (além das premissas) e a conclusão da sua sub-prova atual. Que nem isto aqui: http://i.imgur.com/Us8a1.png Eu estou aí naquele primeiro "...", onde preciso provar C /\ C -> A tendo B e C como hipótese. Se você colar a prova no ProofWeb, você precisa apertar o botão verde "pra baixo" no menu da interface (ou apertar ctrl+, estando no Firefox. Não funciona no Chrome) para o ProofWeb começar a executar o programa. Cada clique na setinha pra baixo representa um passo da prova. Pode-se também voltar, caso se tenha feito algo errado, apertando o botão pra cima. Palavras em verde são aquelas já passadas ao proofweb: para apaga-las, é preciso apertar "pra cima". Clicando na seta com um traço embaixo, você vai até o "final" (ou até o "começo"), é equivalente a clicar na setinha várias vezes. É possível inserir táticas clicando no menu "Backward.." e escolhendo ela (->I por exemplo é a introdução da implicação, etc). Também é possível selecionar Debug - toggle electric terminator para executar uma linha sempre que você a terminar com um . (acho que ajuda, já que faz parte da sintaxe usada) Enfim, a prova em si que eu escrevi é o programa abaixo. Require Import ProofWeb. (* DEMONSTRAR EM DEDUCAO NATURAL: *) Parameter A B C: Prop. Hypothesis P0 : ( ( C /\ C ) -> A ). Hypothesis P1 : ( C \/ ( C /\ A ) ). Theorem T1 : ( ( ( B <-> B ) -> C ) /\ ( B -> A ) ). Proof. con_i. imp_i H. con_e1 A. dis_e (C \/ C /\ A) H1 H2. ass P1. con_i. ass H1. imp_e (C /\ C). ass P0. con_i. ass H1. ass H1. ass H2. imp_i H. con_e2 C. dis_e (C \/ (C /\ A)) H1 H2. ass P1. con_i. ass H1. imp_e (C /\ C). ass P0. con_i. ass H1. ass H1. ass H2. Qed. ___ Logica-l mailing list Logica-l@dimap.ufrn.br http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
Re: [Logica-l] Lógica e Acessibilidade
2012/4/13 Aracele Garcia de Oliveira : > Oi, Elias. Ótimas informações, mas você colocou o ponto certo. > > > "(Mas na verdade, visualizar a "evolução" da prova, apesar de útil, não > é essencial. O fundamental é saber quais são suas hipóteses e o que > você precisa provar, e isto o ProofWeb apresenta como texto) > " > > Colocar o contexto que precisa ser provado e mostrar a prova, sei que várias > ferramentas fazem. Mas o aluno raciocinar, utilizando regras do sistema > dedutivo, por exemplo, para este aluno mesmo criar a prova, aí é que está o > "problema". Pois é o que estou falando, o ProofWeb permite isto! Ele possui um provador de teoremas chamado Coq, que te assiste durante a construção da prova (mostrando se você cometeu algum erro, etc). No nosso caso, até agora, usamos uma teoria de dedução natural com táticas "backward" (partindo da conclusão para chegar até as premissas), e uma teoria semântica escrita por um aluno de JM (o Patrick) que permite demonstrar um modelo onde as premissas são válidas e a conclusão não é, mas sem usar tabela verdade. Veja um exemplo de um exercício em dedução natural "backward" Require Import ProofWeb. Variables A B C : Prop. Theorem example_01 : A /\ B -> B /\ A. Proof. Neste caso, o aluno precisa provar o teorema |- A^B -> B^A sem usar nenhuma hipótese. Ele parte da conclusão, A^B -> B^A, e precisa pensar: poxa, qual foi a regra que permitiu chegar nesta conclusão? Existem várias (você pode chegar até aí através da a eliminação da disjunção, através do absurdo clássico, etc). A resolução deste e de outros exemplos está aqui: http://lolita.dimap.ufrn.br/proofweb/manual-prop.php O tutor decidiu utilizar a regra "introdução da implicação". Com isto, ele digitou: imp_i H. Esta regra é válida! Se assumir como hipótese A ^ B e a partir daí chegar à B ^ A (descartando A ^ B), eu posso introduzir a implicação A ^ B -> B ^ A Neste caso, ele chamou a hipótese de H. Ok, agora precisamos provar B ^ A tendo como hipótese A ^ B. Que regra devemos usar? A regra que o tutor preferiu usar foi a introdução da conjunção con_i. Isto porque se tivermos A e tivermos B, podemos introduzir B ^ A Ok, agora precisamos provar B. Que regra podemos usar para introduzir B? Uma regra é a eliminação da conjunção: con_e2 (A). Agora nós temos A ^ B Mas isto é a nossa hipótese, podemos assumi-la como verdadeira ass H. Agora, provar A. Usamos a eliminação da conjunção, do outro lado: con_e1 (B). Temos A ^ B denovo, que é a hipótese: ass H. Com isto provamos o teorema. A prova completa é: Require Import ProofWeb. (* Exemplos na lógica proposicional *) Variables A B C : Prop. (*Primeiro uma demonstração usando apenas regras "Backward" (para trás - seguindo da conclusão às premissas) *) Theorem example_01 : A /\ B -> B /\ A. Proof. imp_i H. con_i. con_e2 (A). (* Insere um "A" numa conjunção com B *) ass H. con_e1 (B). ass H. Qed. Para realizar esta prova, é necessário pensar sobre as regras da dedução natural. No proofweb existem 150 exercícios de lógica (de coisas simples como P -> P, até coisas não tão simples). Se quiser, você pode tentar resolve-los pelo site: http://lolita.dimap.ufrn.br/proofweb/ ___ Logica-l mailing list Logica-l@dimap.ufrn.br http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
Re: [Logica-l] Lógica e Acessibilidade
A minha experiência com deficientes visuais vem de jogos online conhecidos como "MUDs". MUDs são diferentes da maior parte dos jogos online modernos por terem uma interface somente em texto. Os participantes caminham através de salas (que possuem "descrições"), efetuam ações e interagem socialmente entre si, tudo isso digitando comandos em um terminal. É um jogo bastante imaginativo. MUDs são mais acessíveis à deficientes visuais do que boa parte dos jogos porque os leitores de tela modernos são adequados à leitura de qualquer tipo de texto. O MUD Valinor começou como um projeto voltado à fãs da obra de Tolkien (Senhor dos Anéis e etc), e ainda é, mas acabou voltado também à DVs por serem um público interessado. Eu lembro que no mud em que eu jogava (o MUD Valinor), um problema de acessibilidade eram "mapas" e outras imagens, feitos usando arte ASCII, que apesar de usarem apenas caracteres não são acessíveis à um leitor de tela. A solução adotada foi apresentar também descrições alternativas usando texto puro Olha um exemplo: http://mud.valinor.com.br/articles.php?id=43 A legenda dá pra ler por um leitor de tela, mas o mapa em si não. Um leitor de tela normalmente vai só ler os caracteres especiais (ponto, mais, porcentagem..), sendo portanto inútil. Mas então, programas baseados em texto (e que não possuam essas "imagens") podem ser uma boa escolha. Felizmente, os programas de suporte à lógica que conheço (como o Coq e o Isabelle) são também somente texto. De fato, usar o Coq como interpretador (ou outro programa de "linha de comando") é semelhante, operacionalmente, à jogar em um MUD: você digita comandos e vê o resultado deles. Acessar páginas em um browser também é bastante acessível (com algumas exceções). Um aplicativo web voltado ao ensino da lógica é o ProofWeb. A interface do proofweb é via browser (por exemplo, o Firefox), e ele tem suporte à maioria dos provadores. Eu uso o ProofWeb curso de lógica do João Marcos e Regivan (da UFRN), como interface ao provador Coq. Acredito que o ProofWeb seja acessível à DVs. Ele exibe a "prova" (um programa criado pelo aluno) em um lado, e a saída em outro. À medida que sua prova evolui, ele vai criando árvores de dedução natural. Estas árvores podem ou não ser acessíveis. Porém, o ProofWeb pode mostrar o desenvolvimento com "fitch-style box proofs" que acredito que sejam mais acessíveis. (Mas na verdade, visualizar a "evolução" da prova, apesar de útil, não é essencial. O fundamental é saber quais são suas hipóteses e o que você precisa provar, e isto o ProofWeb apresenta como texto) É possível usar o ProofWeb (selecione "Guest") aqui do grupo de lógica da UFRN: http://lolita.dimap.ufrn.br/proofweb/ Ou no site original, da holanda: http://prover.cs.ru.nl/login.php Alguma documentação: http://lolita.dimap.ufrn.br/proofweb/man.pdf http://lolita.dimap.ufrn.br/proofweb/manual.php http://lolita.dimap.ufrn.br/proofweb/manual-prop.php http://lolita.dimap.ufrn.br/proofweb/tutorial-video.htm Com o ProofWeb, é possível cadastrar alunos em um "curso", enviar exercícios para eles e acompanhar a resolução de forma on-line. Se você checar, existem várias turmas cadastradas no provador da holanda. No momento o ProofWeb daqui só tem duas turmas cadastradas (as duas de cursos de graduação da UFRN), mas já teve uma turma da UFMG. 2012/4/13 Aracele Garcia de Oliveira : > Caros Lógicos desta lista, tudo bem? > Eu gostaria de saber se alguém possui experiência com o ensino de lógica > para pessoas com necessidades visuais (cegos totais ou parciais). > Sabem se existem ferramentas que podem ser utilizadas para o ensino de > tablôs ou calculo de sequentes/dedução natural/etc, por exemplo? > Estou considerando, neste caso, alunos cegos na disciplina de Lógica > Matemática, de um curso de Ciência da Computação. > A tabela verdade pode ser trabalhada através de planilhas, sem problemas. > Sempre realizando as atividades no notebook. > Mas, e no caso de sistemas dedutivos, por exemplo? > Qualquer informação será útil. > Grata ___ Logica-l mailing list Logica-l@dimap.ufrn.br http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
[Logica-l] Lógica e Acessibilidade
Caros Lógicos desta lista, tudo bem? Eu gostaria de saber se alguém possui experiência com o ensino de lógica para pessoas com necessidades visuais (cegos totais ou parciais). Sabem se existem ferramentas que podem ser utilizadas para o ensino de tablôs ou calculo de sequentes/dedução natural/etc, por exemplo? Estou considerando, neste caso, alunos cegos na disciplina de Lógica Matemática, de um curso de Ciência da Computação. A tabela verdade pode ser trabalhada através de planilhas, sem problemas. Sempre realizando as atividades no notebook. Mas, e no caso de sistemas dedutivos, por exemplo? Qualquer informação será útil. Grata -- Att. Aracele Garcia de Oliveira Fassbinder M.Sc. Computer Science - UFSC Professor at Federal Institute Sul de Minas Muzambinho, MG - Brazil Phone: +55 35 8411-9228 Personal Homepage: http://www.inf.ufsc.br/~aracele ___ Logica-l mailing list Logica-l@dimap.ufrn.br http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
Re: [Logica-l] [OT] Vida em Marte!!!
Botei ot de propósito; abre quem quiser. Sent from my iPhone On 13/04/2012, at 11:06, Tony Marmo wrote: > Mais polêmica extra-tópica. O comentário de que não mandaram microscópios > para a missão 36 anos atrás e que o gás liberado pelo experimento PODE ter > sido CO2 (portanto, não sabem ao certo) mostram o quão mal planejado foi o > experimento. O uso de métodos matemáticos como esses para estudar vida aqui > na Terra já é polêmico, quanto mais em outro planeta que se tiver vida, > tem-na em condições diferentes em pontos importantes. > > Em 13 de abril de 2012 07:51, Francisco Antonio Doria > escreveu: > Perdoem o off topic, has essay notícia é boa!!! > > http://www.abc.net.au/science/articles/2012/04/13/3476970.htm?WT.mc_id=science_twitterfeed_latest&utm_source=feedburner&utm_medium=twitter&utm_campaign=Feed%3A+abcscience_latestnews+%28ABC+Science%3A+Latest+News%29 > > -- > fad > > ahhata alati, awienta Wilushati > ___ > Logica-l mailing list > Logica-l@dimap.ufrn.br > http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l > ___ Logica-l mailing list Logica-l@dimap.ufrn.br http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
Re: [Logica-l] [OT] Vida em Marte!!!
Mais polêmica extra-tópica. O comentário de que não mandaram microscópios para a missão 36 anos atrás e que o gás liberado pelo experimento PODE ter sido CO2 (portanto, não sabem ao certo) mostram o quão mal planejado foi o experimento. O uso de métodos matemáticos como esses para estudar vida aqui na Terra já é polêmico, quanto mais em outro planeta que se tiver vida, tem-na em condições diferentes em pontos importantes. Em 13 de abril de 2012 07:51, Francisco Antonio Doria escreveu: > Perdoem o off topic, has essay notícia é boa!!! > > > http://www.abc.net.au/science/articles/2012/04/13/3476970.htm?WT.mc_id=science_twitterfeed_latest&utm_source=feedburner&utm_medium=twitter&utm_campaign=Feed%3A+abcscience_latestnews+%28ABC+Science%3A+Latest+News%29 > > -- > fad > > ahhata alati, awienta Wilushati > ___ > Logica-l mailing list > Logica-l@dimap.ufrn.br > http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l > ___ Logica-l mailing list Logica-l@dimap.ufrn.br http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
[Logica-l] Novo livro do Newton, sobre os fundamentos da mecânica quântica
Newton e eu temos conversado, há muito, sobre os fundamentos da física, e em especial sobre mecânica quântica. Faz uns meses que Newton me envia suas notas a respeito - sobretudo observações epistemológicas, pouca matemática - e sugeri-lhe que, após uma revisão editorial muito light, publicássemos esse material em forma da livro. Conversei com Cesar Benjamim, editor da Contraponto, que topou a parada. As notas finais do Newton me chegaram ontem, e vou logo começar o trabalho editorial. Tá ***MUITO*** interessante! -- fad ahhata alati, awienta Wilushati ___ Logica-l mailing list Logica-l@dimap.ufrn.br http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
[Logica-l] [OT] Vida em Marte!!!
Perdoem o off topic, has essay notícia é boa!!! http://www.abc.net.au/science/articles/2012/04/13/3476970.htm?WT.mc_id=science_twitterfeed_latest&utm_source=feedburner&utm_medium=twitter&utm_campaign=Feed%3A+abcscience_latestnews+%28ABC+Science%3A+Latest+News%29 -- fad ahhata alati, awienta Wilushati ___ Logica-l mailing list Logica-l@dimap.ufrn.br http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
