Demostració automàtica de teoremes

La demostració automàtica de teoremes (de sigles ATP, pel terme en anglés: Automated theorem proving), que també pot ser denominada deducció automatizado, és actualment el subcampo més desenrollat del raonament automàtic, i s'encarrega de la demostració de teoremes matemàtiques per mig de programes d'ordenador.

Definició

Les tècniques de demostració automàtica de teoremes consistixen en aplicar métodos computacionals per a demostrar teoremes. És dir, demostració de teoremes en un ordenador. Estes tècniques són especialment viables com a ferramenta per a demostrar teoremes de geometria plana.

En llínees generals, el procediment és el següent:

1. La teorema a demostrar es traduïx en térmens algebraics: tant les hipòtesis com la tesis s'expressen com a condicions del tipo $P_i(x_1,\dots ,x_n)=0,i=1,\dots ,k$ i $Q(x_1,\dots ,x_n)=0$ respectivament.
2. La veracitat de la teorema és llavors equivalent a que $Q$ estiga en l'ideal generat per $P_1,\dots ,P_k$ (lo que equival a que l'anulació de $P_1,\dots ,P_k$ en un punt implique l'anulació de $Q$ en eixe punt).
3. El problema de pertinença d'un polinomi a un ideal és un problema clàssic en àlgebra computacional; una tècnica habitual de resolució d'este problema és el càlcul d'una base de Gröbner adequada.

Este método de demostració té l'inconvenient de que la complexitat computacional del problema de pertinença és elevada.

El problema de deduir una teorema

Depenent de la llògica subjacent, el problema de decidir sobre si una teorema és vàlida o no, varia des de ser una tasca trivial a impossible. Per al cas freqüent de la llògica proposicional, el problema és deduible pero NP-complet, i per lo tant es creu que solament existixen algoritmes de temps exponencial per a les tasques generals de la prova. Per a un càlcul de predicat de primer orde, que no posseïx cap axioma apropiat el Teorema de la completitud de Gödel indica que les teoremes són exactament les fòrmules ben formades llògicament vàlides, aixina que l'identificació de teoremes és recurrentemente enumerable, és dir que en recursos illimitats eventualment tot teorema vàlida poden ser demostrat. Les proposicions inválidas, és dir les fòrmules que no són exigides per una teoria donada, no sempre poden ser reconegudes. Ademés, una teoria formal consistent que conté la teoria de primer orde dels número natural (o siga que té certs axioma apropiats), per la teorema de l'estat incomplet de Gödel, conté una proposició verdadera que no pot ser demostrada, en este cas un "demostrador" de la teorema que intenta demostrar tal proposició conclou en un punt indefinit.

En estos casos, un demostrador de primer orde de la teorema pot no poder terminar mentres que busca una demostració. A pesar d'estos llímits teòrics, els demostradores pràctics de la teorema poden solucionar molts problemes difícils en estes llògiques.

Referències

Traducció de la Wikipedia en idioma anglés