> 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
> =========================================================================
>