A demonstração automatizada de teoremas (cuja sigla em inglês é ATP, ou dedução automática) é um sub-campo da área da Ciência da Computação e da Lógica que lida com o problema de provar teoremas matemáticos através de programas de computador. O raciocínio automatizado para uma demonstração matemática foi uma das áreas de maior interesse e ímpeto para o desenvolvimento da ciência dos computadores.
Fundamentos lógicos Enquanto as raízes da lógica formal datam do tempo de Aristóteles, o fim do século XIX e início do século XX testemunharam o desenvolvimento da lógica moderna e da matemática formalizada. O trabalho de Gottlob Frege, Begriffsschrift (1879),Frege, Gottlob (1879). Begriffsschrift. Verlag Louis Neuert. introduziu um cálculo proposicional completo bem como o que constitui essencialmente a lógica moderna de predicados. Um outro trabalho de Frege publicado em 1884, Os Fundamentos da Aritmética,Frege, Gottlob (1884). Die Grundlagen der Arithmetik (PDF). Breslau: Wilhelm Kobner. exprime partes da matemática em lógica formal. Esta abordagem foi continuada por Russell e Whitehead no seu trabalho Principia Mathematica, primeiramente publicado em 1910-1913,Bertrand Russell; Alfred North Whitehead (1910–1913). Principia Mathematica (1st ed.). Cambridge University Press. com uma edição revista de 1927,Bertrand Russell; Alfred North Whitehead (1927). Principia Mathematica (2nd ed.). Cambridge University Press. e que foi um trabalho de grande influência na altura. Bertrand Russell e Alfred North Whitehead pensavam que conseguiriam deduzir toda a verdade matemática usando axiomas e regras de inferência da lógica formal, abrindo assim em princípio o processo de automatização. Em 1920, Thoralf Skolem simplificou um resultado de Leopold Löwenheim, que conduziu ao teorema de Löwenheim-Skolem e, em 1930, à noção de universo Herbrand e interpretação de Herbrand que permitiu que a satisfabilidade (ou o contrário) de primeira-ordem para fórmulas (e assim a respetiva validade de um teorema) ficasse reduzida ao problema da satisfabilidade de problemas proposicionaisHerbrand, Jaques (1930). Recherches sur la théorie de la démonstration. (potencialmente muitos desses problemas).
Em 1929, Mojżesz Presburger mostrou que a teoria aritmética de Presburger (aritmética que é gerada pelas sentenças que podem ser formadas com {números pertencentes a N, +, =}) não dá origem a expressões exteriores ao conjunto de todas essas sentenças (teoria que tem a propriedade da decidabilidade) e fez um algoritmo que podia determinar a veracidade de uma dada sentença nessa aritmética.Presburger, Mojżesz (1929). "Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt". Comptes Rendus du I congrès de Mathématiciens des Pays Slaves (Warszawa): 92–101.Davis, Martin (2001), "The Early History of Automated Deduction", in Robinson, Alan; Voronkov, Andrei, Handbook of Automated Reasoning 1, Elsevier) No entanto, um pouco após este resultado positivo, Kurt Gödel publicou o trabalho sobre as proposições não decidíveis dos Principia Mathematica e Sistemas Relacionados (1931), mostrando que em qualquer sistema axiomático suficientemente forte existem teoremas que não podem ser demonstrados dentro desse sistema. Este tópico foi depois desenvolvido em 1920 por Alonzo Church e Alan Turing, que por um lado, deram definições independentes mas equivalentes de computação, e por outro, deram exemplos concretos para questões sobre as quais era impossível decidir sobre a sua demonstrabilidade.
Primeiras implementações Logo após a Segunda Guerra Mundial, os primeiros computadores de uso geral apareceram. Em 1954, Martin Davis programou um algoritmo de Presburger para um computador JOHNNIAC no Instituto de Estudos Avançados de Princeton. De acordo com Davis “o seu maior triunfo foi provar que a soma de dois números pares é um número par”.Bibel, Wolfgang (2007). "Early History and Perspectives of Automated Deduction" (PDF). KI 2007. LNAI (Springer) (4667): 2–18. Acessado em 2 de setembro de 2012. Um projeto mais ambicioso foi a Teoria Lógica das Máquinas, um sistema dedutivo para a lógica proposicional dos Principia Mathematica, desenvolvido por Allen Newell, Herbert A. Simon e J. C. Shaw. Também podendo ser implementado num JOHNNIAC, a Teoria Lógica da Máquinas construiu demonstrações a partir de um conjunto pequeno de axiomas proposicionais e três regras de dedução: modus ponens, substituição de variáveis proposicionais, e atribuição definicional a fórmulas. O sistema utilizou guiões para heurísticas e conseguiu demonstrar 38 dos primeiros 52 teoremas dos Principia.
A abordagem heurística da Teoria Lógica das Máquinas, tentou emular matemáticos (humanos), não conseguindo garantir que uma demonstração podia ser encontrada para cada teorema válido. Em contraste, com outros algoritmos mais sistemáticos é conseguida completude de primeira-ordem, pelo menos teórica. Abordagens iniciais apoiaram-se nos resultados de Herbrand e Skolem para converter uma fórmula de primeira-ordem em conjuntos cada vez maiores de formulae proposicional através da instanciação de variáveis com termos de um universo Herbrand. As fórmulas proposicionais podiam então ser verificadas para a sua não-satisfabilidade usando certos métodos. O programa de Gilmore usou a conversão da forma normal disjuntiva, a forma na qual a satisfabilidade de uma fórmula é óbvia.Gilmore, Paul (1960). "A proof procedure for quantification theory: its justification and realisation". IBM Journal of Research and Development 4: 28–35. doi:10.1147/rd.41.0028.
Decidabilidade e computação Tal como acontece com o conceito de um conjunto decidível, a definição de uma teoria decidível ou sistema lógico pode ser dada tanto em termos de métodos eficazes ou em termos de funções computáveis. Estes são geralmente considerados equivalentes pela Tese de Church. De fato, a demonstração de que um sistema lógico ou de que uma teoria é indecidível, usa a definição formal de computabilidade para mostrar que um determinado conjunto não é um conjunto decidível, e depois utiliza a tese de Church para mostrar que a teoria ou sistema lógico não é decidível por qualquer método eficaz (Enderton 2001, pp 206ff.).
Problemas relacionados Um problema mais simples embora relacionado é o problema de verificação de demonstrações, em que uma demonstração para um teorema é certificada como válida. Para isso, é genericamente requerido que cada passo individual da demonstração possa ser verificado por uma função primitiva recursiva ou programa, e dessa maneira o programa tem a propriedade da decidabilidade.
Dado que as demonstrações geradas por um teorema automatizado são usualmente em grande número, o problema da compressão é crucial e várias técnicas que têm vindo a ser desenvolvidas têm como objetivo tornar esse número mais pequeno, e consequentemente mais facilmente compreendido e verificável.
Os programas para assistir computadores a fazer demonstrações requerem ajuda humana na forma de sugestões. Dependendo do grau de automatização, o demonstrador pode ficar reduzido essencialmente a um verificador de demonstrações, com o utilizador providenciando a demonstração de uma maneira formal ou, tarefas de demonstração podem ser feitas automaticamente. Demonstradores interativos são utilizados para tarefas diversas, mas mesmo os sistemas mais automatizados demonstraram um número de teoremas interessantes e difíceis, incluindo pelo menos um que tem escapado aos matemáticos, nomeadamente a Conjectura de Robins.W.W. McCune (1997). "Solution of the Robbins Problem". Journal of Automated Reasoning 19 (3).Gina Kolata (December 10, 1996). "Computer Math Proof Shows Reasoning Power". The New York Times. Retrieved 2008-10-11. No entanto, estes sucessos são esporádicos, e trabalhar em problemas difíceis requer um utilizador proficiente.
Uma outra distinção é por vezes feita entre demonstração de teoremas e outras técnicas, onde um processo é considerado demonstração se consiste numa demonstração lógica, começando com axiomas e produzindo novos passos inferenciais usando regras de inferência. Outras técnicas incluiriam verificação de modelos, as quais, no caso mais simples, incluem o método da enumeração por força bruta dos numerosos estados possíveis (embora a implementação atual de verificadores de modelos requeira muita esperteza, e não se reduza somente à força bruta).
Existem sistemas híbridos de demonstração de teoremas que usam verificação de modelos como uma regra de inferência. Existem também programas que foram escritos para demonstrar um teorema em particular, como uma demonstração (na maioria das vezes informal) que caso seja levada a cabo pelo programa, acabando num dado resultado, atribui ao teorema veracidade. Um bom exemplo deste tipo de demonstração é a do Teorema das Quatro Cores cuja demonstração depende de um computador, e que levantou controvérsias depois de ser declarada como uma demonstração que era essencialmente impossível de verificar por humanos dado o grande número de cálculos que o programa teve de fazer (tais demonstrações são chamadas demonstrações que não se podem verificar). Outro exemplo é o do jogo Conecta Quatro em que o primeiro a jogar ganha.
Usos industriais O uso comercial de demonstradores automatizados para teoremas concentra-se em desenho de circuitos integrados e verificação. Desde o vírus Pentium FDIV, os complicados pontos unidade de superfície dos microprocessadores modernos foram desenhados com maior cuidado. AMD, Intel e outros utilizam a demonstração automatizada de teoremas para verificar que divisão e outras operações são corretamente implementadas nos seus processadores.
Demonstração de teoremas de primeira ordem No fim dos anos 60 agências financiando a pesquisa em dedução automatizada começaram a privilegiar as aplicações práticas. Uma das área mais frutuosas foi a de verificação de programas enquanto que teoremas de primeira ordem eram aplicados ao problema de verificar a correção de programas de computador em linguagens como Pascal, Ada, Java, etc.. De entre os sistemas de verificação de programas o mais notável era o Verificador de Pascal de Standford desenvolvido por David Luckham na Universidade de Standford. Este era baseado no Standford Resolution Prover também desenvolvido em Standford usando o princípio de resolução de J. A. Robinson. Este foi o primeiro sistema de dedução automática a demonstrar habilidade em resolver problemas matemáticos e que foi anunciado na seção das Notícias da Sociedade Americana de Matemática antes das soluções serem formalmente publicadas.
Demonstrações de primeira ordem para teoremas é um dos sub-campos do campo das demonstrações automatizadas de teoremas. A lógica é suficientemente expressiva para permitir a especificação arbitrária de problemas, frequentemente de uma forma razoavelmente natural e intuitiva. Por outro lado, a sua decidibilidade é ainda não completa, e um número sólido e completo de cálculos foram desenvolvidos, permitindo sistemas completamente automatizados. Lógicas mais expressivas, tais como lógicas de ordem superior, permitem exprimir de forma mais conveniente uma banda mais larga de problemas do que a lógica de primeira ordem, mas a demonstração de teoremas nessas lógicas é menos desenvolvida.
Plataformas e competições A qualidade de sistemas implementados tem beneficiado da existência de uma grande biblioteca de exemplos de plataformas standard – A Biblioteca de Problemas: Os Milhares de Problemas sobre Demonstradores de TeoremasSutcliffe, Geoff. "The TPTP Problem Library for Automated Theorem Proving". Retrieved 8 September 2012. (TPTP em inglês) — bem como o Sistema de Competição CADE ATP (CASC em inglês), uma competição anual de sistemas de primeira ordem para muitas classes de problemas de primeira ordem importantes.