> s�o demonstrados de forma similares.
>
> Eu sei que essa maneira de demonstrar via "compila��o"
> de todos os casos � meio "tosca", mas
> ser� que n�o pode ser interessante em problemas muito dif�cieis?
>
> Neste exemplo houve uma s�rie de expans�es de termos usando fatos
> conhecidos.
> Exemplo: Prove que 7(pq+qr+pr)<=2+9pqr.
> 7(p+q+r)(pq+qr+rp) <= 2(p+q+r)^3 + 9pqr
>
> Note que 2 = 2.1 foi expandido.
>
> Um provador autom�tico de teoremas feito em Prolog, por exemplo
> poderia fazer essas expans�es.O problema seria ele saber
> exatamente *o que* expandir. � exatamente a� que entra o desafio, o
> sentimento e
> a criatividade.
>
>
> Uma vez estava conversando com um amigo meu que estava terminando seu
> doutorado em an�lise.
> Ele havia concordado comigo que na matem�tica tudo s�o fatos e regras
> como na linguagem Prolog.
> Para quem n�o conhece Prolog: http://en.wikipedia.org/wiki/Prolog
>
> Ent�o n�o era dif�cil construir provadores de teorema que pudessem
> responder quest�es mais ou menos
> simples via aplica��o de regras. Mas h� um problema: Cada axioma/hip�tese
> do teorema � uma regra e
> cada teorema no banco de dados do programa � uma regra.
>
> Se f�ssemos usar a for�a bruta e aplicar
> todas as regras indiscriminadamente isso iria gera uma explos�o combinat�ria
> de senten�as e dificilmente
> chegar�amos a solu��o ou a conclus�o da verdade/falsidade do teorema
> chegando em regras at�micas que
> por hip�tese e/ou teoremas anteriores sabemos ser verdadeiras.
>
> Claro que se soub�ssemos quais regras expandir, n�o precisar�amos de
> computador... como nesse exerc�cio.
>
>
>
>
>
>
> =========================================================================
> Instru��es para entrar na lista, sair da lista e usar a lista em
> http://www.mat.puc-rio.br/~nicolau/olimp/obm-l.html
> =========================================================================
>