2012/4/13 Aracele Garcia de Oliveira <[email protected]>: > 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 [email protected] http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
