Demostració automàtica de teoremes
La demostració automatitzada de teoremes (també coneguda com ATP o deducció automatitzada) és un subcamp del raonament automatitzat i la lògica matemàtica que s'ocupa de la demostració de teoremes matemàtics mitjançant programes informàtics. El raonament automatitzat sobre la demostració matemàtica va ser un factor de motivació important per al desenvolupament de la informàtica.
Fonaments lògics
[modifica]Mentre que les arrels de la lògica formalitzada es remunten a Aristòtil, el final del segle XIX i principis del XX van veure el desenvolupament de la lògica moderna i les matemàtiques formalitzades. El Begriffsschrift de Frege (1879) va introduir tant un càlcul proposicional complet com el que és essencialment la lògica de predicats moderna.[1] Els seus Fonaments de l'Aritmètica, publicats el 1884, [2] expressaven (parts de) les matemàtiques en lògica formal. Aquest enfocament va ser continuat per Russell i Whitehead en els seus influents Principia Mathematica, publicats per primera vegada entre 1910 i 1913, [3] i amb una segona edició revisada el 1927.[4] Russell i Whitehead van pensar que podien derivar tota la veritat matemàtica utilitzant axiomes i regles d'inferència de la lògica formal, en principi obrint el procés a l'automatització. El 1920, Thoralf Skolem va simplificar un resultat anterior de Leopold Löwenheim, donant lloc al teorema de Löwenheim–Skolem i, el 1930, a la noció d'un univers d'Herbrand i una interpretació de Herbrand que permetia la (insatisfacció) de les fórmules de primer ordre (i, per tant, la validesa d'un teorema) que es redueix a (potencialment infinitat) la satisfacció proposicional problemes.[5]
L'any 1929, Mojżesz Presburger va demostrar que la teoria de primer ordre dels nombres naturals amb suma i igualtat (ara anomenada aritmètica de Presburger en el seu honor) és decidible i va donar un algorisme que podia determinar si una frase determinada en el llenguatge era vertadera o falsa.[6][7]
Tanmateix, poc després d'aquest resultat positiu, Kurt Gödel va publicar On Formally Undecidible Propositions of Principia Mathematica and Related Systems (1931), mostrant que en qualsevol sistema axiomàtic prou fort, hi ha afirmacions vertaderes que no es poden demostrar en el sistema. Aquest tema va ser desenvolupat més en els anys 30 per Alonzo Church i Alan Turing, que d'una banda van donar dues definicions independents però equivalents de computabilitat, i de l'altra van donar exemples concrets de preguntes indecidibles.
Primeres implementacions
[modifica]Poc després de la Segona Guerra Mundial, es van disposar els primers ordinadors de propòsit general. El 1954, Martin Davis va programar l'algoritme de Presburger per a un ordinador de tubs de buit JOHNNIAC a l' Institut d'Estudis Avançats de Princeton, Nova Jersey. Segons Davis, "el seu gran triomf va ser demostrar que la suma de dos nombres parells és parell".[8][9] Més ambiciós va ser el Logic Theorist el 1956, un sistema de deducció per a la lògica proposicional dels Principia Mathematica, desenvolupat per Allen Newell, Herbert A. Simon i JC Shaw. També funcionant amb un JOHNNIAC, el teòric de la lògica va construir demostracions a partir d'un petit conjunt d'axiomes proposicionals i tres regles de deducció: modus ponens, substitució de variables (proposicionals) i la substitució de fórmules per la seva definició. El sistema va utilitzar una guia heurística i va aconseguir demostrar 38 dels primers 52 teoremes dels Principia.[8]
L'enfocament "heurístic" del teòric de la lògica va intentar emular els matemàtics humans, i no va poder garantir que es pogués trobar una demostració per a cada teorema vàlid ni tan sols en principi. En canvi, altres algorismes més sistemàtics van aconseguir, almenys teòricament, la completitud per a la lògica de primer ordre. Els enfocaments inicials es basaven en els resultats d'Herbrand i Skolem per convertir una fórmula de primer ordre en conjunts successivament més grans de fórmules proposicionals mitjançant la instanciació de variables amb termes de l'univers Herbrand. Aleshores, les fórmules proposicionals es podrien comprovar si no són satisfactòries mitjançant diversos mètodes. El programa de Gilmore va utilitzar la conversió a la forma normal disjuntiva, una forma en què la satisfacció d'una fórmula és òbvia.[10][11]
Decidabilitat del problema
Segons la lògica subjacent, el problema de decidir la validesa d'una fórmula varia de trivial a impossible. Per al cas comú de la lògica proposicional, el problema és decidible però co-NP-complet, i per tant només es creu que existeixen algorismes de temps exponencial per a tasques de demostració generals. Per a un càlcul de predicats de primer ordre, el teorema de completitud de Gödel estableix que els teoremes (enunciats demostrables) són exactament les fórmules ben formades semànticament vàlides, de manera que les fórmules vàlides són computablement enumerables : donats recursos il·limitats, qualsevol fórmula vàlida es pot provar. Tanmateix, les fórmules no vàlides (les que no estan implicades per una teoria determinada), no sempre es poden reconèixer.
L'anterior s'aplica a les teories de primer ordre, com ara l'aritmètica de Peano. Tanmateix, per a un model específic que pot ser descrit per una teoria de primer ordre, algunes afirmacions poden ser certes però indecidibles en la teoria utilitzada per descriure el model. Per exemple, pel teorema d'incompletezza de Gödel, sabem que qualsevol teoria consistent els axiomes de la qual són certs per als nombres naturals no pot demostrar que totes les afirmacions de primer ordre són certes per als nombres naturals, fins i tot si es permet que la llista d'axiomes sigui enumerable infinit. Es dedueix que un demostrador de teoremes automatitzat no s'acabarà mentre cerca una demostració precisament quan l'enunciat que s'està investigant és indecidible en la teoria que s'utilitza, encara que sigui cert en el model d'interès. Malgrat aquest límit teòric, a la pràctica, els provadors de teoremes poden resoldre molts problemes difícils, fins i tot en models que no estan completament descrits per cap teoria de primer ordre (com els nombres enters).
Problemes relacionats
[modifica]Un problema més senzill, però relacionat, és la verificació de la prova, on una demostració existent per a un teorema es certifica vàlida. Per a això, generalment cal que cada pas de prova individual es pugui verificar mitjançant una funció o programa recursiu primitiu i, per tant, el problema és sempre decidible.
Atès que les demostracions generades pels demostradors de teoremes automatitzats solen ser molt grans, el problema de la compressió de proves és crucial i s'han desenvolupat diverses tècniques destinades a fer que la sortida del provador sigui més petita i, per tant, més fàcil d'entendre i comprovar.
Els assistents de prova requereixen que un usuari humà doni pistes al sistema. Depenent del grau d'automatització, el provador es pot reduir essencialment a un verificador de proves, amb l'usuari proporcionant la prova de manera formal, o es poden fer tasques de prova importants de manera automàtica. Els provadors interactius s'utilitzen per a una varietat de tasques, però fins i tot els sistemes totalment automàtics han demostrat una sèrie de teoremes interessants i durs, inclòs almenys un que ha eludit els matemàtics humans durant molt de temps, és a dir, la conjectura de Robbins.[12] Tanmateix, aquests èxits són esporàdics i treballar en problemes difícils sol requerir un usuari competent.
De vegades es fa una altra distinció entre la demostració de teoremes i altres tècniques, on un procés es considera com una demostració de teoremes si consisteix en una demostració tradicional, començant amb axiomes i produint nous passos d'inferència utilitzant regles d'inferència. Altres tècniques inclourien la verificació de models, que, en el cas més simple, implica l'enumeració de força bruta de molts estats possibles (tot i que la implementació real dels verificadors de models requereix molta intel·ligència i no es redueix simplement a la força bruta).
Hi ha sistemes híbrids de demostració de teoremes que utilitzen la verificació de models com a regla d'inferència. També hi ha programes que es van escriure per demostrar un teorema particular, amb una prova (generalment informal) que si el programa acaba amb un determinat resultat, aleshores el teorema és cert. Un bon exemple d'això va ser la demostració assistida per màquina del teorema dels quatre colors, que va ser molt controvertida com la primera prova matemàtica afirmada que era essencialment impossible de verificar pels humans a causa de l'enorme mida del càlcul del programa (aquestes proves s'anomenen proves no-enquestables). Un altre exemple de prova assistida per programa és el que demostra que la partida de Connect Four sempre la pot guanyar el primer jugador.
Aplicacions
[modifica]L'ús comercial de la demostració automatitzada de teoremes es concentra principalment en el disseny i la verificació de circuits integrats. Des de l'error Pentium FDIV, les complicades unitats de punt flotant dels microprocessadors moderns s'han dissenyat amb un escrutini addicional. AMD, Intel i altres utilitzen teoremes automatitzats per verificar que la divisió i altres operacions s'implementen correctament als seus processadors.
Altres usos dels demostradors de teoremes inclouen la síntesi de programes, la construcció de programes que compleixin una especificació formal.[13] Els demostradors de teoremes automatitzats s'han integrat amb assistents de demostració, incloent Isabelle/HOL.[14]
Les aplicacions dels demostradors de teoremes també es troben en el processament del llenguatge natural i la semàntica formal, on s'utilitzen per analitzar les representacions del discurs.
Referències
[modifica]- ↑ Frege, Gottlob. Begriffsschrift (en anglès). Verlag Louis Neuert, 1879.
- ↑ Frege, Gottlob. Die Grundlagen der Arithmetik (en anglès). Breslau: Wilhelm Kobner, 1884.
- ↑ Russell, Bertrand. Principia Mathematica (en anglès). 1st. Cambridge University Press, 1910–1913.
- ↑ Russell, Bertrand. Principia Mathematica (en anglès). 2a edició. Cambridge University Press, 1927.
- ↑ Recherches sur la théorie de la démonstration (Tesi) (en francès), 1930.
- ↑ Presburger, Mojżesz Comptes Rendus du I Congrès de Mathématiciens des Pays Slaves [Warszawa], 1929, pàg. 92–101.
- ↑ Davis, Martin. «The Early History of Automated Deduction». A: Robinson & Voronkov 2001 (en anglès), 2001.
- ↑ 8,0 8,1 Davis, Martin. «The Early History of Automated Deduction». A: Robinson & Voronkov 2001 (en anglès), 2001.
- ↑ Bibel, Wolfgang Ki 2007, 4667, 2007, pàg. 2–18 [Consulta: 2 setembre 2012].
- ↑ Davis, Martin. «The Early History of Automated Deduction». A: Robinson & Voronkov 2001 (en anglès), 2001.
- ↑ Gilmore, Paul IBM Journal of Research and Development, 4, 1960, pàg. 28–35. DOI: 10.1147/rd.41.0028.
- ↑ McCune, W. W. Journal of Automated Reasoning, 19, 3, 1997, pàg. 263–276. DOI: 10.1023/A:1005843212881.
- ↑ Basin, D. «Synthesis of programs in computational logic». A: M. Bruynooghe and K.-K. Lau. Program Development in Computational Logic (en anglès). 3049. Springer, 2004, p. 30–65 (LNCS).
- ↑ Meng, Jia; Paulson, Lawrence C. (en anglès) Journal of Automated Reasoning, 40, 1, 01-01-2008, pàg. 35–60. DOI: 10.1007/s10817-007-9085-y. ISSN: 1573-0670.