2012/4/13 Elias Gabriel Amaral da Silva <[email protected]>: > 2012/4/13 Aracele Garcia de Oliveira <[email protected]>: > 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+<seta pra baixo>, 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 [email protected] http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
