61
edits
Changes
no edit summary
== 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.
#'''Metodo de Prova'''
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 '''¬''' ao invés de '''not'''. Em seguida, vão alguns exemplos do uso de operadores booleanos inativos:
Nos preocupamos agora em determinar como o maple simplifica expressões booleanas
caso estejam combinadas. Começamos com um simples exemplo de dupla negação:
Isto pode ser simplificado através do uso da função bsimp do maple.
Agora, seguimos para um exemplo mais complexo,no qual o leitor pode confirmar a corretude da simplificação, construindo uma tabela verdade.
O próximo exemplo ilustra a simplificação do Modus Ponens. Primeiro afirmamos que p implica q e p é verdadeiro.
Então simplificamos a expressão booleana
Determinando que q e p são verdadeiros, como nós já sabíamos que p era verdadeiro, nós concluímos que q é verdadeiro.
A função '''bsimp''' é um simplificador geral para expressões booleanas construídas usando os operadores booleanos inativos. A função computa uma expressão booleana simplificada equivalente ao seu argumento. Podemos também usar o maple para determinar se uma expressão é uma tautologia através do uso da função tautology oferecida pelo pacote lógico.
Agora mostramos como usar o maple para compreender algumas provas construtivas. Especificamente, vamos examinar como explorar a construção de uma lista sequencial de números compostos
Enquanto o maple pode ser usado para gerar uma lista de '''n''' inteiros compostos consecutivos, gerados por prova, não é possível derivar a prova em si usando o maple. Devemos observar que este argumento não fornece o menor conjunto de n inteiros compostos consecutivos. Embora dado um inteiro positivo '''n''', é possível usar o maple para encontrar a menor sequencia de '''n''' inteiros compostos consecutivos.
Através do maple abordaremos a prova não construtiva da existência de um número infinito de números primos. Por ser uma prova não construtiva, não podemos simplesmente criar um algoritmo para gerar um número primo maior, assumindo a existência de um número primo máximo. Embora a ideia chave da prova seja considerar a primalidade do inteiro '''N! +1''', é possível que '''N!+1''' seja por si só um número primo, porém mesmo que não seja seu maior fator primo deve ser maior que n. É possível encontrar o menor fator primo fatorando '''N!+1''' diretamente, usando a rotina '''ifactor''' da biblioteca maple.
Podemos observar pelo resultado que, enquanto alguns desses números são primos, outros não são, a partir disso, podemos fazer a leitura do menor fator primo.
Para determinar o menor fator primo de cada um desses inteiros, podemos escrever a seguinte rotina:
Ela usa o procedimento '''factorset''' do pacote numtheory para computar o conjunto de fatores do inteiro de entrada, e então simplesmente seleciona seu menor membro.
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.
#Indução Matemática
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.
Através da geração de um grande conjunto de dados numéricos de pouca compreensão, eventualmente será possível determinar a fórmula acima. A saída mostra que n² é um pouco menos que o dobro da soma dos n primeiros inteiros para os valores de n testados. Partindo de um padrão, é possível perceber que a fórmula correta é uma função quadrática de n, resolva para encontrar os coeficientes e então teste se esse procedimento produz a fórmula correta.
Uma técnica útil para experimentos semelhantes é gerar listas de pares que consista da sequencia que esteja interessado e de várias possibilidades que você elabore. Para investigar a hipótese de que a fórmula seja quadrática, devemos começar gerando uma lista de pares semelhantes ao seguinte:
Para explorar se a soma é uma função quadrática de n, podemos inserir um quadrático genérico em n e solucionar para encontrar os coeficientes a,b e c. precisamos de três equações para serem solucionadas em busca dos três coeficientes
Agora, instruímos o maple para resolver essas equações e encontrar os três coeficientes.
A nossa fórmula original torna-se:
Neste ponto, as habilidades do maple permitem manipular expressões simbolicamente para ajudar a construir uma prova indutiva. Segue um exemplo de como a prova interativa da fórmula acima pode ser conduzido no maple por indução matemática.
O termo geral da soma é:
Enquanto o lado direito da fórmula é:
Podemos usar o procedimento subs para verificar o passo base da indução; neste caso o passo base é n=1