% (find-angg "LATEX/2013-GA-criterios.tex")
% (find-dn4ex "edrx08.sty")
% (find-angg ".emacs.templates" "s2008a")
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2013-GA-criterios.tex && latex    2013-GA-criterios.tex"))
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2013-GA-criterios.tex && pdflatex 2013-GA-criterios.tex"))
% (eev "cd ~/LATEX/ && Scp 2013-GA-criterios.{dvi,pdf} edrx@angg.twu.net:slow_html/LATEX/")
% (defun d () (interactive) (find-dvipage "~/LATEX/2013-GA-criterios.dvi"))
% (find-dvipage "~/LATEX/2013-GA-criterios.dvi")
% (find-pspage  "~/LATEX/2013-GA-criterios.ps")
% (find-pspage  "~/LATEX/2013-GA-criterios.pdf")
% (find-xpdfpage "~/LATEX/2013-GA-criterios.pdf")
% (find-zsh0 "cd ~/LATEX/ && dvipdf         2013-GA-criterios.dvi 2013-GA-criterios.pdf")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o 2013-GA-criterios.ps 2013-GA-criterios.dvi")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 600 -P pk -o 2013-GA-criterios.ps 2013-GA-criterios.dvi && ps2pdf 2013-GA-criterios.ps 2013-GA-criterios.pdf")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o tmp.ps tmp.dvi")
% (find-pspage  "~/LATEX/tmp.ps")
% (ee-cp "~/LATEX/2013-GA-criterios.pdf" (ee-twupfile "LATEX/2013-GA-criterios.pdf") 'over)
% (ee-cp "~/LATEX/2013-GA-criterios.pdf" (ee-twusfile "LATEX/2013-GA-criterios.pdf") 'over)
% (find-twusfile     "LATEX/" "2013-GA-criterios")
% http://angg.twu.net/LATEX/2013-GA-criterios.pdf
\documentclass[oneside]{book}
\usepackage[latin1]{inputenc}
\usepackage{edrx08}       % (find-dn4ex "edrx08.sty")
%L process "edrx08.sty"  -- (find-dn4ex "edrx08.sty")
\input edrxheadfoot.tex   % (find-dn4ex "edrxheadfoot.tex")
\begin{document}

\input {stem}.dnt


As notas da correção não são tão justas quanto eu
gostaria. Se eu fosse ser totalmente objetivo 

A regra de que a

  Todos sabem que depois de provas da Engenharia durante as quais os
  alunos podem ir no banheiro o espelho do banheiro e alguns outros
  lugares do PURO ficam cheios de papeizinhos com cola.



MUITAS pessoas responderam questões da prova (a VS) que exigiam
{\it demonstrações} com {\it contas}. Eu enfatizei em muitos
pontos do curso que demonstrações têm uma estrutura precisa,
da mesma forma que programas de computador têm uma estrutura
precisa e uma sintaxe rígida (a que o computador entende).




\section{Construções são parecidas com programas}

Todo mundo está mais ou menos familiar com a idéia de
"programa". Considerem o seguinte problema:

\begin{quote}
  Seja $x$ um número real em $[-1,1]$. Obtenha um ponto da forma
  $(x,y)$ no círculo unitário.
\end{quote}

Uma coisa é dizer: ``resolva $x^2+y^2=1$''; outra é dizer

\begin{quote}
  seja $y:=sqrt(1-x^2)$; o ponto $(x,y)$ está no círculo unitário
\end{quote}

e, opcionalmente, dependendo do leitor pra quem estamos escrevendo,
incluir uma conta que mostre que neste caso temos $x^2+y^2=1$.

Acho que eu consegui deixar {\it razoavelmente} claro no curso como
"construções" correspondem a "programas". Poucos alunos do PURO
já usaram linguagens para computação simbólica que
conseguem manipular expressões como "$x^2+y^2=1$" e aí executar
passos como (este exemplo é do Maxima):

\begin{verbatim}
  solve (x^2 + y^2 = 1, x);
\end{verbatim}

que retorna:

\begin{verbatim}
                   2                 2
  [x = - sqrt(1 - y ), x = sqrt(1 - y )]
\end{verbatim}

e aposto R\$\,20 que nenhum {\it aluno} do PURO já teve que _programar_ um
sistema de computação simbólica capaz de resolver
equações não-lineares, ou mesmo alterar um já existente...
mas pelo menos quase todos os professores e veteranos de exatas no
PURO têm bem claro o quanto estas coisas são difíceis,
dependeram de muitas décadas de pesquisa pesada e são
praticamente impossíveis de aprender em um semestre, mas no entanto
qualquer aluno que já tenha terminado Prog 1 sabe interpretar um
programa equivalente a:

\begin{verbatim}
  x = readnumber()
  y = sqrt(1 - x*x)
  print(x, y)
\end{verbatim}

ou seja, sabe que a idéia de "\code{y:=sqrt(1-x^2)}" é _simples_.





\section{Demonstrações}

Neste semestre que acabou de acabar (2012.2) acho que já consegui
deixar bastante claro como devem funcionar certos tipos de
demonstrações - principalmente as que são sequências de
igualdades e as tipo "lista 1 do Reginaldo", que são de
afirmações do tipo "todo $X$ tem a propriedade $P(X)$". Ainda não
deu pra deixar claro o suficiente, pra gente suficiente, que numa
afirmação como

  \begin{narrow}
  a hipérbole $H_1$ está contida em $H_2$
  \end{narrow}

o "leitor-padrão" espera, _automaticamente_, um algoritmo que
receba um ponto qualquer, "A", de H_1, e a partir dele produza uma
prova de que este ponto A pertence a H_2. O único modo 100% honesto
- já vou explicar o que eu quero dizer com "100% honesto" - de
mostrar pra todo mundo como esse leitor-padrão funciona é
formalizar uma linguagem na qual uma expressão como

  "Proposição: o conjunto C está contido no conjunto D.
   Demonstração:"

só possa ser seguida por um algoritmo que começa com um ponto
qualquer de C e termina com uma prova de que este ponto pertence a
D...

O caminho que me parece mais viável pra implementar isto é
estender um "proof assistant" que entende uma sintaxe parecida com um
Inglês simplificado - possivelmente o miz3, que é uma
extensão do HOL... só que a teoria por trás de "proof
assistants" é {\it muito} mais difícil que a dos sistemas de
computação simbólica! - pra esse proof assistant estendido
entender as expressões que a gente usa em GA; isto pode ajudar a
convencer os alunos que quando a gente fala de demonstrações bem
escritas a gente não está chutando.

Só que pra chegarmos a este ponto vai dar bastante trabalho -
"aprender HOL e {\tt miz3} e implementar uma linguagem para GA neles"
é um projeto de pesquisa de tamanho médio... e na situação
atual está muito difícil fazer pesquisa no PURO.




\section{O que eu quero que aconteça}

Queremos que em dois anos muitas dezenas de alunos da Engenharia e da
Computação saibam fazer demonstrações bem e escrevê-las
também muito bem, e centenas saibam mais ou menos. Quando isto
acontecer muitas idéias que hoje os alunos consideram "difíceis"
vão passar a ser "óbvias" - e vai ser possível tirar
dúvidas básicas com qualquer pessoa de exatas que você
encontre nos corredores, como em qualquer universidade decente.

Aí também vai ficar bem mais fácil criarmos eletivas
avançadas e projeto de iniciação científica, e fazermos
pesquisa, seminários, etc. A situação vai ficar {\it bem}
menos deprimente.


\section{O que eu quero que NÃO tenha mais como acontecer}




\end{document}

% Local Variables:
% coding:           raw-text-unix
% ee-anchor-format: "«%s»"
% End: