Changes

== Introdução ==

Neste capítulo descreveremos como o maple pode ser usado para ajudar na compreensão e construção de provas matemáticas. Capacidades computacionais podem não parecer particularmente relevantes para o estudo das provas, embora na realidade essas capacidades possam ser úteis em provas de várias maneiras. Neste capítulo, descrevemos como o maple pode ser útil para trabalhar com regras formais de inferência, descrevemos como pode ajudar a compreender provas construtivas e não construtivas. Além disso, mostramos como usar o maple para ajudar a desenvolver provas usando indução matemática, até mesmo mostrando sua utilidade para ambos o passo base e passo indutivo, na prova da fórmula de somatório. Ademais, mostraremos como o maple pode ser usado para computar termos de sequencias definidas recursivamente. Vamos também comparar a eficiência da geração de termos dessa sequencia via técnicas indutivas versus técnicas recursivas.

Embora o maple não possa receber teoremas e resultados de provas para esses teoremas, pode receber expressões lógicas e simplificadas ou determinar características tais como: se uma expressão booleana pode ser satisfeita ou se é uma tautologia. Para trabalhar com expressões lógicas no maple, precisamos usar alguns dos recursos oferecidos pelo pacote de '''logic'''(um assunto abordado de maneira mais aprofundada no capítulo 9).

Primeiramente examinaríamos os operadores lógicos: conjunção, disjunção, negação e '''implicação'''. Não existe (no Maple). Para estudar as condicionais, devemos trabalhar com os operadores booleanos inativos oferecidos pelo pacote de '''logic'''. Todos esses são iniciados com o caracter '''mexpr''' '''&''', por exemplo: usamos '''&and''' ao invés de '''and''' e '''&not''' ao invés de '''not'''. Em seguida, vão alguns exemplos do uso de operadores booleanos inativos:

Agora confrontamos nosso exemplo final do uso do maple explorando teoremas matemáticos. Neste caso vamos explorar a conjectura de Goldbach: que é, todo inteiro par maior que 4 pode ser expressado como a soma de dois primos.

O maple pode ser usado para auxiliar na elaboração de provas de várias afirmações matemáticas usando a indução matemática. De fato, com o maple como seu assistente, você pode conduzir inteiramente o processo de descoberta e averiguação de forma intuitiva. É provável que entre os primeiros exemplos de indução matemática, encontremos a verificação da fórmula '''1+2+3+...+n = n(n+1)/2''',a soma dos primeiros n inteiros positivos. O maple se adequa para provar fórmulas como essa porque os passos envolvidos numa prova indutiva incluem manipulação simbólica. É possível gerar uma grande quantidade de dados numéricos para serem examinados.

Usando um pouco de manipulação algébrica, vemos que as duas últimas fórmulas são iguais. Isso completa a prova via indução matemática. Concluímos que nosso palpite sobre a fórmula está correto.

As funções do maple podem ser definidas tanto processualmente (usando a função '''proc''') como explicitamente (usando a notação '''->'''), cada um desses métodos envolve meios interativos e recursivos de definição. Iniciamos nosso estudo, usando a função '''->''' do maple. Se nós quiséssemos definir uma função polinomial '''A(n)= 3n³ + 41n²- 3n + 101''' nós usaríamos o seguinte comando:

Que é comparável às vezes obtidas para '''f2'''. Note que a implementação puramente recursiva '''f1''' não possibilita o uso para '''f2(100)'''. De fato, um bom exercício é mostrar que para fazê-lo, '''f2''' precisaria de aproximadamente '''f2(99)''' chamadas para operar todos os subcasos que surgirem. Mesmo a um bilhão de subcasos por segundo, isso exigiria mais de seis mil anos para sua conclusão.

Nesta seção do material, exploraremos o modo como o maple pode ser usado para resolver as questões 4,5 e 8 da seção “computações e explorações” do livro.

Para determinar quantos pares de números primos existem, usaremos o pacote '''numtheory''' do maple, que contém as funções nextprime, '''prevprime''' e '''ithprime'''

Parece não haver um padrão óbvio ocorrendo.

Primeiro vamos gerar dados para trabalhá-los (manipulá-los).

Você pode tentar averiguar se esse padrão persiste, substituindo 500 na definição de '''fib_list''' por números muito maiores. (o teste da divisibilidade por 111, nós deixamos pra você).

Agora escrevemos uma função que fará a iteração da função Collatz até que o valor obtido seja igual a 1, nós incluímos uma variável 'count' por dois motivos: Primeiro, queremos ter uma idéia de quanto tempo leva para que as iterações estabilizem; Segundo, já que não sabemos ao certo se as iterações vão estabilizar para um dado valor de entrada 'seed', nos codificamos um limite superior para o número de iterações a serem computadas.