Demonstração Automatizada de Teoremas

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), 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, 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, com uma edição revista de 1927, 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 proposicionais (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. 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”. 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.

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. 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 (Benchmarks ou plateaux) 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 Teoremas (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.

Alguns sistemas importantes (todos tendo ganho pelo menos uma divisão da Competição CADE ATP) estão listados abaixo:

• E é um demonstrador de alto desempenho para lógica de primeira ordem completa, mas construído num cálculo puramente equacional, desenvolvido primariamente em raciocínio automatizado por um grupo de cientistas da Universidade Técnica de Munique.
• Otter, desenvolvido no Laboratório Nacional de Argonne, é baseado em resolução de primeira ordem para paramodulação. Otter foi substituído pelo Prover9, o qual é colocado a par com o Mace4.
• SETHEO é um sistema de alto desempenho baseado no cálculo de um modelo de eliminação dirigido. É desenvolvido pelo grupo de raciocínio automatizado da Universidade Técnica de Munique. E e Setheo foram combinados (com outros sistemas) dando origem ao compositor de teoremas E-SETHEO.
• Vampiro é desenvolvido e implementado na Universidade de Manchester por Andrei Voronkov e Krystof Hoder, e anteriormente por Alexandre Riazanov. Ganhou a Competição Sistema CADE ATP na mais prestigiosa divisão CNF (MIX) em 1999, e de 2001 a 2010.
• Waldmeister é um sistema especializado em lógica de primeira ordem para equacionar unidades. Ganhou a divisão CASC UEQ de 1997 a 2010.
• SPASS é um sistema de primeira ordem de demonstração de problemas que contém igualdade. É desenvolvido pelo grupo de investigação Automatização da Lógica do Instituto Max Planck para Ciência dos Computadores.

Técnicas Populares

• Resolução de primeira ordem com unificação
• Demonstração de Teoremas de Lean
• Eliminação de modelos
• Método de análise de plataformas
• Superposição e reescrita de termos
• Verificação de modelos
• Indução matemática
• Diagramas de decisão binária
• DPLL
• Unificação de ordem superior
• Comparação

Assistente de Demonstração

• Comparação e categoria: [1]

Software gratuito

• Alt-erg
• Automath
• CVC
• E
• Gödel Machines
• iProver
• IsaPlanner
• Demonstrador de Teoremas KED
• leanCoP
• LCF
• LoTREC
• MetaPRL
• NuPRL
• Paradox
• Simplify (GPL’ed desde 5/2011)
• Twelf
• SPARK (linguagem de programação)
• Proprietário de software
• Acumen RuleManager (produto comercial)
• ALLIGATOR
• Carine
• Kiv (gratuito, plugin para Eclipse)
• Prover Plug-In (produto comercial)
• ProverBox
• ResearchCyc
• Demonstrador de teoremas de aritmética modular

Pessoas com notabilidade no campo

• Leo Bachmair, co-desenvolvedor do cálculo de sobreposição
• Woody Bledsoe, pioneiro da AA
• Robert S. Boyer, co-autor do demonstrador de teoremas Boyer Moore, co-recipiente do Herbrand Award 1999.
• Alan Bundy, Universidade de Edimburgo, raciocínio de nível superior para guiar demonstração indutiva, planeamento de demonstrações e recipiente de 2007 Prêmio IJCAI por Excelência em Pesquisa. Prémio Herbrand, e Prémio Donal E. Walker por serviço de distinção.
• William McCune, Laboratório Nacional de Argonne, autor do Otter, o primeiro demonstrador de teoremas de alto desempenho. Muitos artigos importantes, recipiente do Prémio Herbrand 2000.
• Hubert Comon, CNRS e agora ENS Cachan. Com muito artigos importantes.
• Robert Lee Constable, Universidade de Cornell. Contribuições importantes em teoria dos tipos, VuPRL.
• Martin Davis, autor do livro mestre do raciocínio artificial, co-inventor do algoritmo DPLL, recipiente do Prémio Herbrand 2005.
• Branden Fitelson, Universidade da Califórnia em Berkeley. Trabalho na descoberta automatizada das bases axiomáticas mais rápidas para sistemas lógicos.
• Harald Ganzinger, co-desenvolvedor do cálculo de sobreposição, director do MPI Saarbrüken 2004 (póstumo)
• Michael Genesereth, professor de Ciências da computação da Universidade de Standford
• Keith Goolsbey, investigador da máquina de inferência do Cyc.
• Michael J. C. Gordon, diretor no desenvolvimento do demonstrador de teoremas HOL.
• Gérard Huet, reescrita de termos, lógica HOL, Prémio Herbrand 1998.
• Robert Kowalski, desenvolveu o demonstrador de teoremas conetor de gráficos e a resolução SLD, a máquina de inferência que executa programas lógicos.
• Donald W. Loveland, Universidade de Duke. Autor e co-desenvolvedor do procedimento DPLL, desenvolvedor do modelo de eliminação, recipiente do Prémio Herbrand 2001.
• David Luckham, Universidade de Standford, desenvolveu o demonstrador de teoremas para resolução de Standford em 1968, o primeiro sistema de dedução automatizado utilizado para resolver problemas anunciado na secção da Notícias da Associação Americana de Matemática, e subsequentemente desenvolveu o verificador de Pascal, o primeiro programa de verificação de sistemas para Pascal, amplamente distribuído, 1968-75.
• Norman Megill, desenvolvedor do Metamath, e responsável pelo site metamath.org, uma base de dados online de demonstrações verificadas automaticamente.
• J Strother Moore, co-autor do demonstrador de teoremas Boyer-Moore, co-recipiente do Prémio Herbrand 1999.
• Robert Nieuwenhuis, Universidade de Barcelona. Co-desenvolvedor do cálculo de sobreposição.
• Tobias Niokow, Universidade Técnica de Munique, contribuições para reescrita (de ordem superior), co-desenvolvedor do assistente de demonstrações Isabelle.
• Ross Over Beek, Laboratório Nacional Argonne, fundador da Bolsa de Investigação para a Interpretação de Genomas.
• Lawrence C. Paulson, Universidade de Cambridge, com trabalho no sistema lógico de ordem superior, co-desenvolvedor do auxiliador de teoremas Isabelle.
• David Plaisted, Universidade da Carolina do Norte em Chapel Hill; com resultados complexos, contribuições para reescrita e completude, demonstrador de teoremas baseados em instâncias.
• John Rushby, diretor do programa – SRI International.
• J. Alan Robinson, Universidade de Siracusa; desenvolveu uma resolução e unificação original baseada na demonstração de teoremas de primeira ordem, co-editor do Manual de Raciocínio Automatizado, recipiente do Prémio Herbrand 1996.
• Jürgen Schimidhuber, com trabalho nas Máquinas de Gödel: Resolvedores de Problemas Universais, Auto-Referenciais Que Fazem Auto-Melhoramentos Optimais Prováveis.
• Stephan Schulz, Demonstrador de Teoremas E.
• Natarajan Shankar, SRI International. Recipiente do Prémio Herbrand 2002.
• Geoff Sutcliffe, Universidade de Miami. Curador da Coleção TPTP, e organizador do concurso anual CADE.
• Dolph Ulrich, Universidade de Purdue, com trabalho na descoberta automatizada de bases de axiomas para sistemas.
• Robert Veroff, Universidade do Novo México. Com muito artigos significativos no campo.
• Andrei Voronkov, Desenvolvedor do Vampiro e Co-editor do Livro Mestre de raciocínio automatizado.
• Larry Wos, Laboratório Nacional Argonne, com muitos artigos significativos no campo. Primeiro Prémio Herbrand 1992.
• Wen-Tsun Wu, trabalho na demonstração de teoremas geométricos: Método de Wu, Prémio Herbrand 1992.
• Christopher Weidenbach, autor do SPASS, demonstrador de teoremas automatizado.

Ver também

1. Computação simbólica
2. Demonstração assistida por computador
3. Raciocínio automatizado
4. Verificação Formal
5. Programação Lógica
6. Verificador de demonstrações
7. Verificação de Modelos
8. Complexidade de demonstrações
9. Sistema de álgebra computacional
10. Análise de programas (CC)
11. Resolvedor geral de problemas
12. Metamath – linguagem para matemática formalizada

Referências

1. Chin-Liang Chang; Richard Char-Tung Lee (1973). Symbolic Logic and Mechanical Theorem Proving. Academic Press.´
2. Enderton, Herbert (2001), A mathematical introduction to logic (2nd ed.), Boston, MA: Academic Press, ISBN 978-0-12-238452-3
3. Loveland, Donald W. (1978). Automated Theorem Proving: A Logical Basis. Fundamental Studies in Computer Science Volume 6. North-Holland Publishing.
4. Luckham, David (1990). Programming with Specifications: An Introduction to Anna, A Language for Specifying Ada Programs. Springer-Verlag Texts and Monographs in Computer Science, 421 pp.
5. Gallier, Jean H. (1986). Logic for Computer Science: Foundations of Automatic Theorem Proving. Harper & Row Publishers (Available for free download).
6. Duffy, David A. (1991). Principles of Automated Theorem Proving. John Wiley & Sons.
7. Wos, Larry; Overbeek, Ross; Lusk, Ewing; Boyle, Jim (1992). Automated Reasoning: Introduction and Applications (2nd ed.). McGraw–Hill.
8. Alan Robinson and Andrei Voronkov (eds.), ed. (2001). Handbook of Automated Reasoning Volume I & II. Elsevier and MIT Press.
9. Fitting, Melvin (1996). First-Order Logic and Automated Theorem Proving (2nd ed.). Springer.