Prova automática de teorema

Prova automatizada de teoremas (também conhecida como ATP ou dedução automatizada) é um subcampo do raciocínio automatizado e da lógica matemática que lida com a demonstração de teoremas matemáticos por programas de computador. O raciocínio automatizado sobre a prova matemática foi um grande impulso para o desenvolvimento da ciência da computação.

Fundamentos lógicos

Enquanto as raízes da lógica formalizada remontam a Aristóteles, o final do século XIX e início do século XX viu o desenvolvimento da lógica moderna e da matemática formalizada. O Begriffsschrift de Frege (1879) introduziu um cálculo proposicional completo e o que é essencialmente a lógica de predicados moderna. Seu Fundamentos da Aritmética, publicado em 1884, expressava (partes da) matemática na lógica formal. Essa abordagem foi continuada por Russell e Whitehead em seu influente Principia Mathematica, publicado pela primeira vez em 1910–1913, e com uma segunda edição revisada em 1927. Russell e Whitehead pensaram que poderiam derivar toda a verdade matemática usando axiomas e inferência regras da lógica formal, em princípio abrindo o processo à automatização. Em 1920, Thoralf Skolem simplificou um resultado anterior de Leopold Löwenheim, levando ao teorema de Löwenheim-Skolem e, em 1930, à noção de um universo de Herbrand e uma interpretação de Herbrand que permitia a (in)satisfabilidade de fórmulas de primeira ordem (e, portanto, a validade de um teorema) a serem reduzidos a (potencialmente infinitos) problemas de satisfazibilidade proposicionais.

Em 1929, Mojżesz Presburger mostrou que a teoria dos números naturais com adição e igualdade (agora chamada de aritmética de Presburger em sua homenagem) é decidível e forneceu um algoritmo que poderia determinar se uma determinada sentença no idioma era verdadeira ou falsa. No entanto, logo após este resultado positivo, Kurt Gödel publicou On Formally Undecidable Propositions of Principia Mathematica and Related Systems (1931), mostrando que em qualquer sistema axiomático suficientemente forte existem afirmações verdadeiras que não podem ser provadas no sistema. Este tópico foi desenvolvido na década de 1930 por Alonzo Church e Alan Turing, que por um lado deram duas definições independentes, mas equivalentes de computabilidade, e por outro deram exemplos concretos para questões indecidíveis.

Primeiras implementações

Logo após a Segunda Guerra Mundial, os primeiros computadores de uso geral tornaram-se disponíveis. Em 1954, Martin Davis programou o algoritmo de Presburger para um computador de tubo de vácuo JOHNNIAC no Instituto de Estudos Avançados em Princeton, Nova Jersey. De acordo com Davis, "seu grande triunfo foi provar que a soma de dois números pares é par". Mais ambicioso foi o Logic Theory Machine em 1956, um sistema de dedução para a lógica proposicional do Principia Mathematica, desenvolvido por Allen Newell, Herbert A. Simon e J. C. Shaw. Também rodando em um JOHNNIAC, a Logic Theory Machine construiu provas a partir de um pequeno conjunto de axiomas proposicionais e três regras de dedução: modus ponens, substituição de variável (proposicional) e a substituição de fórmulas por sua definição. O sistema usou orientação heurística e conseguiu provar 38 dos primeiros 52 teoremas do Principia.

A "heurística" A abordagem da Teoria da Lógica Machine tentou imitar os matemáticos humanos e não podia garantir que uma prova pudesse ser encontrada para cada teorema válido, mesmo em princípio. Em contraste, outros algoritmos mais sistemáticos alcançaram, pelo menos teoricamente, a integridade da lógica de primeira ordem. As abordagens iniciais basearam-se nos resultados de Herbrand e Skolem para converter uma fórmula de primeira ordem em conjuntos sucessivamente maiores de fórmulas proposicionais, instanciando variáveis com termos do universo de Herbrand. As fórmulas proposicionais poderiam então ser verificadas quanto à insatisfabilidade usando vários métodos. O programa de Gilmore usou a conversão para a forma normal disjuntiva, uma forma na qual a satisfatibilidade de uma fórmula é óbvia.

Decidibilidade do problema

Dependendo da lógica subjacente, o problema de decidir a validade de uma fórmula varia de trivial a impossível. Para o caso frequente de lógica proposicional, o problema é decidível, mas co-NP-completo e, portanto, acredita-se que existam apenas algoritmos de tempo exponencial para tarefas de prova geral. Para um cálculo de predicado de primeira ordem, o teorema da completude de Gödel afirma que os teoremas (declarações prováveis) são exatamente as fórmulas bem formadas logicamente válidas, portanto, a identificação de fórmulas válidas é recursivamente enumerável: dados recursos ilimitados, qualquer fórmula válida pode eventualmente ser comprovado. Entretanto, fórmulas inválidas (aquelas que não estão vinculadas a uma dada teoria), nem sempre podem ser reconhecidas.

O acima se aplica a teorias de primeira ordem, como a aritmética de Peano. No entanto, para um modelo específico que pode ser descrito por uma teoria de primeira ordem, algumas afirmações podem ser verdadeiras, mas indecidíveis na teoria usada para descrever o modelo. Por exemplo, pelo teorema da incompletude de Gödel, sabemos que qualquer teoria cujos axiomas próprios sejam verdadeiros para os números naturais não pode provar que todas as afirmações de primeira ordem são verdadeiras para os números naturais, mesmo que a lista de axiomas próprios seja infinita. enumerável. Segue-se que um provador de teoremas automatizado falhará ao terminar enquanto procura por uma prova precisamente quando a afirmação que está sendo investigada é indecidível na teoria que está sendo usada, mesmo que seja verdadeira no modelo de interesse. Apesar desse limite teórico, na prática, os provadores de teoremas podem resolver muitos problemas difíceis, mesmo em modelos que não são totalmente descritos por nenhuma teoria de primeira ordem (como os números inteiros).

Problemas relacionados

Um problema mais simples, mas relacionado, é a verificação de prova, onde uma prova existente para um teorema é certificada como válida. Para isso, geralmente é necessário que cada etapa de prova individual possa ser verificada por uma função ou programa recursivo primitivo e, portanto, o problema é sempre decidível.

Uma vez que as provas geradas pelos provadores de teoremas automatizados são tipicamente muito grandes, o problema da compressão da prova é crucial e várias técnicas com o objetivo de tornar a saída do provador menor e, consequentemente, mais facilmente compreensível e verificável, foram desenvolvidas.

Assistentes de prova requerem um usuário humano para dar dicas ao sistema. Dependendo do grau de automação, o provador pode ser essencialmente reduzido a um verificador de prova, com o usuário fornecendo a prova de maneira formal, ou tarefas significativas de prova podem ser executadas automaticamente. Provadores interativos são usados para uma variedade de tarefas, mas mesmo sistemas totalmente automáticos provaram uma série de teoremas interessantes e difíceis, incluindo pelo menos um que iludiu os matemáticos humanos por muito tempo, ou seja, a conjectura de Robbins. No entanto, esses sucessos são esporádicos e o trabalho em problemas difíceis geralmente requer um usuário proficiente.

Outra distinção às vezes é feita entre prova de teorema e outras técnicas, onde um processo é considerado prova de teorema se consistir em uma prova tradicional, começando com axiomas e produzindo novos passos de inferência usando regras de inferência. Outras técnicas incluiriam a verificação de modelo, que, no caso mais simples, envolve a enumeração de força bruta de muitos estados possíveis (embora a implementação real de verificadores de modelo exija muita inteligência e não reduza simplesmente à força bruta).

Existem sistemas híbridos de prova de teoremas que usam a verificação de modelo como uma regra de inferência. Existem também programas que foram escritos para provar um determinado teorema, com uma prova (geralmente informal) de que se o programa terminar com um determinado resultado, então o teorema é verdadeiro. Um bom exemplo disso foi a prova assistida por máquina do teorema das quatro cores, que foi muito controversa como a primeira prova matemática reivindicada que era essencialmente impossível de verificar por humanos devido ao enorme tamanho do cálculo do programa (como provas são chamadas de provas não pesquisáveis). Outro exemplo de prova assistida por programa é aquele que mostra que o jogo do Connect Four sempre pode ser ganho pelo primeiro jogador.

Usos industriais

O uso comercial da prova automatizada de teoremas concentra-se principalmente no projeto e verificação de circuitos integrados. Desde o bug do Pentium FDIV, as complicadas unidades de ponto flutuante dos microprocessadores modernos foram projetadas com escrutínio extra. AMD, Intel e outros usam prova de teorema automatizada para verificar se a divisão e outras operações estão implementadas corretamente em seus processadores.

Prova de teorema de primeira ordem

No final da década de 1960, as agências que financiavam pesquisas em dedução automatizada começaram a enfatizar a necessidade de aplicações práticas. Uma das primeiras áreas frutíferas foi a de verificação de programas em que os provadores de teoremas de primeira ordem foram aplicados ao problema de verificar a exatidão de programas de computador em linguagens como Pascal, Ada, etc. Notável entre os primeiros sistemas de verificação de programas foi o Stanford Pascal Verifier desenvolvido por David Luckham na Universidade de Stanford. Isso foi baseado no Stanford Resolution Prover também desenvolvido em Stanford usando o princípio de resolução de John Alan Robinson. Este foi o primeiro sistema de dedução automatizada a demonstrar a capacidade de resolver problemas matemáticos anunciados nos Avisos da American Mathematical Society antes que as soluções fossem formalmente publicadas.

A prova de teoremas de primeira ordem é um dos subcampos mais maduros da prova automatizada de teoremas. A lógica é expressiva o suficiente para permitir a especificação de problemas arbitrários, muitas vezes de forma razoavelmente natural e intuitiva. Por outro lado, ainda é semi-decidível, e uma série de cálculos sólidos e completos foram desenvolvidos, permitindo sistemas totalmente automatizados. Lógicas mais expressivas, como lógicas de ordem superior, permitem a expressão conveniente de uma gama mais ampla de problemas do que a lógica de primeira ordem, mas a prova de teoremas para essas lógicas é menos desenvolvida.

Comparativos, competições e fontes

A qualidade dos sistemas implementados beneficiou-se da existência de uma grande biblioteca de exemplos de referência padrão — a Biblioteca de Problemas dos Milhares de Problemas para Demonstradores de Teoremas (TPTP) —, bem como do CADE ATP System Competition (CASC), um evento anual competição de sistemas de primeira ordem para muitas classes importantes de problemas de primeira ordem.

Alguns sistemas importantes (todos venceram pelo menos uma divisão de competição CASC) estão listados abaixo.

• E é um provador de alto desempenho para a lógica de primeira ordem completa, mas construído sobre um cálculo puramente equacional, originalmente desenvolvido no grupo de raciocínio automatizado da Universidade Técnica de Munique sob a direção de Wolfgang Bibel, e agora na Universidade Estadual Cooperativa de Baden-Württemberg em Stuttgart.
• Otter, desenvolvido no Laboratório Nacional de Argonne, é baseado na resolução de primeira ordem e paramodulação. Otter foi substituído por Prover9, que é emparelhado com Mace4.
• SETHEO é um sistema de alto desempenho baseado no cálculo de eliminação de modelo direcionado para o objetivo, originalmente desenvolvido por uma equipe sob direção de Wolfgang Bibel. E e SETHEO foram combinados (com outros sistemas) no teorema composto provador E-SETHEO.
• Vampire foi originalmente desenvolvido e implementado na Universidade de Manchester por Andrei Voronkov e Krystof Hoder. É agora desenvolvido por uma equipe internacional crescente. Ele ganhou a divisão FOF (entre outras divisões) no CADE ATP System Competition regularmente desde 2001.
• Waldmeister é um sistema especializado para a lógica unit-equacional de primeira ordem desenvolvida por Arnim Buch e Thomas Hillenbrand. Ganhou a divisão UEQ da CASC por catorze anos consecutivos (1997-2010).
• SPASS é um primeiro provador de teorema de lógica de ordem com igualdade. Isso é desenvolvido pelo grupo de pesquisa Automation of Logic, Max Planck Institute for Computer Science.

O Theorem Prover Museum é uma iniciativa para conservar as fontes dos sistemas provadores de teoremas para análise futura, uma vez que são importantes artefactos culturais/científicos. Tem as fontes de muitos dos sistemas mencionados acima.

Técnicas populares

• Resolução de primeira ordem com a unificação
• Eliminação do modelo
• Método de tableaux analítico
• Superposição e reescrever termo
• Verificação de modelo
• Indução matemática
• Diagramas de decisão binários
• DPLL
• Unificação de ordem superior

Sistemas de software

Software gratuito

• Alt-Ergo
• Automatização
• CVC
• E
• GKC
• Máquina de Gödel
• IProver
• IsaPlanner
• Prova de teorema KED
• Copo magro
• Leão II
• LCF
• Logictools online theorem prover
• LÍTRCE
• MetaPRL
• Mizarro.
• NuPRL
• Paradoxo
• Prover9
• PVS
• Simplificar
• SPARK (linguagem de programação)
• Twelf
• Prover de teorema Z3

Software proprietário

• Acumen RuleManager (produto comercial)
• ALLIGATOR (CC BY-NC-SA 2.0 UK)
• CARACTERÍSTICA
• KIV (livremente disponível como um plugin para Eclipse)
• Plug-in Prover (produto do motor à prova comercial)
• ProverBox
• Wolfram Mathematica
• Investigação
• Prova de teorema de aritmética modular de Spear