Prova automática de teoremas
Origem: Wikipédia, a enciclopédia livre.
Prova automática de teoremas (PAT) ou dedução automática, atualmente a sub-área mais desenvolvida do raciocínio automatizado (RA), é a prova de teoremas matemáticos por um programa de computador.
Índice |
[editar] Decidibilidade do problema
Dependendo da lógica subjacente, o problema de decidir a validade de um teorema varia do trivial ao impossível. Para o caso freqüente da lógica proposicional, o problema é decidível mas NP-completo, e portanto se acredita que apenas algoritmos com complexidade de tempo exponencial existam para tarefas de prova gerais. Para um cálculo de predicados de primeira ordem, isto é, não tendo nenhum axioma próprio, o Teorema da Completude de Gödel afirma que os teoremas são exatamente as fórmulas bem formadas, portanto identificar teoremas é recursivamente enumerável, isto é, dados recursos ilimitados, qualquer teorema válido pode eventualmente ser provado. Sentenças inválidas, isto é, fórmulas que não são conseqüência de uma dada teoria, nem sempre podem ser reconhecidas. Além disso, uma teoria formal consistente que contém a teoria de primeira ordem dos números naturais (tendo portanto certos axiomas próprios), pelo Teorema da incompletude de Gödel, contém uma sentença verdadeira que não pode ser provada, caso no qual um provador de teoremas tentando provar tal sentença não termina sua execução.
Nestes casos, um provador de teoremas de primeira ordem pode falhar em terminar ao procurar por uma prova. Apesar destes limites teóricos, provadores de teorema na prática são capazes de resolver muitos problemas difíceis nestas lógicas.
