Saltar para o conteúdo

Prova automática de teoremas

Origem: Wikipédia, a enciclopédia livre.
Trecho de uma prova em agda2

Prova automática de teoremas (PAT) ou dedução automática (DA) é a prova de teoremas matemáticos por um programa de computador. É atualmente a sub-área mais desenvolvida do raciocínio automatizado (RA).

Decidibilidade do problema

[editar | editar código-fonte]

Dependendo da lógica subjacente, o problema de decidir a validade de um teorema varia do trivial ao impossível. Para o caso freqüente da lógica proposicional, o problema é decidível mas NP-completo, e portanto se acredita que apenas algoritmos com complexidade de tempo exponencial existam para tarefas de prova gerais. Para um cálculo de predicados de primeira ordem, isto é, não tendo nenhum axioma próprio, o teorema da completude de Gödel afirma que os teoremas são exatamente as fórmulas bem formadas, portanto identificar teoremas é recursivamente enumerável, isto é, dados recursos ilimitados, qualquer teorema válido pode eventualmente ser provado. Sentenças inválidas, isto é, fórmulas que não são conseqüência de uma dada teoria, nem sempre podem ser reconhecidas. Além disso, uma teoria formal consistente que contém a teoria de primeira ordem dos números naturais (tendo portanto certos axiomas próprios), pelo teorema da incompletude de Gödel, contém uma sentença verdadeira que não pode ser provada, caso no qual um provador de teoremas tentando provar tal sentença não termina sua execução.

Nestes casos, um provador de teoremas de primeira ordem pode falhar em terminar ao procurar por uma prova. Apesar destes limites teóricos, provadores de teorema na prática são capazes de resolver muitos problemas difíceis nestas lógicas.

Princípios da Lógica

[editar | editar código-fonte]

Enquanto as raízes da lógica formal vêm de lógica aristotélica, no final do século XIX e início do século XX aconteceu o desenvolvimento da lógica moderna e da matemática formal. Begriffsschrift (1879), de Gottlob Frege, introduziu tanto a lógica proposicional como o que é essencialmente a lógica de predicados moderna.[1] Seu Os Fundamentos da Aritmética, publicado em 1884,[2] expressam (partes da) matemática na lógica formal. Esta abordagem foi continuada por Russell e Whitehead em seu influente Principia Mathematica, publicado pela primeira vez em 1910-1913,[3] e revisado em sua segunda edição em 1927.[4] Russell e Whitehead pensaram que podiam derivar toda a verdade matemática utilizando axiomas e regras de inferência da lógica formal, abrindo caminhos para o processo de 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 do Universo de Herbrand e a uma Interpretação de Herbrand que permitia (in)satisfiabilidade das fórmulas da lógica de primeira ordem (e portanto, a validade de um teorema) para serem reduzidas a (potencialmente infinitos) problemas de satisfatibilidade proposicional.[5]

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 honra) é decidabilidade e deu um algoritmo que pode determinar se uma sentença dada neta linguagem era verdadeira ou falsa.[6][7] Entretanto, pouco tempo após esse resultado positivo, Kurt Gödel publicou On Formally Undecidable Propositions of Principia Mathematica e Related Systems (1931), mostrando que em todo sistema axiomático fortemente baseado existem sentenças que são verdadeiras e que não podem ser provadas.Este tema foi desenvolvido na década de 1930 por Alonzo Church e Alan Turing, quem por um lado deu duas definições independentes e equivalentes da computabilidade, e por outro deu exemplos concretos para questões indecidíveis.

Primeiras Implementações

[editar | editar código-fonte]

Pouco tempo após a Segunda Guerra Mundial, o primeiro general decidiu que os computadores deveriam ficar acessíveis. Em 1954, Martin Davis programou o algoritmo de Presburger para um JOHNNIAC, um computador de tubos de vácuo pertencente à Princeton Institute for Advanced Study. De acordo com Davis, "É um grande triunfo provar que a soma de dois números pares também é par".[7][8] A Máquina de Teoria Lógica era mais ambiciosa, um sistema de dedução matemática para a lógica proposicional de Principia Mathematica, desenvolvido por Allen Newell, Herbert A. Simon e J. C. Shaw. Este também rodava em um JOHANNIAC, a máquina de Lógica Teórica construiu provas a partir de uma pequeno conjunto de axiomas e três regras de dedução: modus ponens, substituição de variáveis proposicionais, e a substituição de de fórmulas por suas definições. O sistema usava orientação heurística, e tentando, conseguiu provar 38 dos primeiros 52 teoremas presentes em Principia.[7]

A aproximação "heurística" da Máquina de Lógica Teórica tentou emular o raciocínio humano, e não conseguia garantir que uma prova podia ser encontrada para cada teorema válido a priori. Em contraste, outro, mas algoritmos mais sistemáticos alcançaram, pelo menos teoricamente, incompletude para a lógica de primeira ordem.

Abordagens iniciais contavam com os resultados de Herbrand e Skolem para converter uma fórmula de primeira ordem em conjuntos sucessivamente maiores de fórmulas proposicionais por instanciar as variáveis com os termos da Universo de Herbrand . As fórmulas proposicionais puderam então ser verificadas para insatisfiabilidade usando uma série de métodos. O epigrama de Gilmore usou conversão para forma normal disjuntiva e uma forma onde a satisfabilidade da fórmula tornou-se óbvia.[7][9]

Decibilidade de um problema

[editar | editar código-fonte]

Dependendo da lógica subjacente, o problema de decidir a validade de uma fórmula varia do trivial ao impossível. Para o caso freqüente da lógica proposicional, o problema é decidível, porém Co-NP-complete, acredita-se que existam apenas algoritmos em tempo exponencial para tarefas de prova. Para a primeira ordem de cálculo predicativo, com nenhum axioma próprio, o Teorema da Incompletude de Gödel afirma que qualquer fórmula válida pode ser comprovada.

Entretanto, fórmulas inválidas não podem sempre serem reconhecias e além disso, uma teoria formal consistente que contem lógica de primeira ordem dos números naturais (contendo alguns "axiomas adequados"), por Teorema de incompletude de Gödel, contém sentenças verdadeiras que não podem ser provadas. Nestes casos, uma prova automatizada do teorema pode vir a falhar, pois poderá nunca encontrar uma resposta. Apesar destes limites teóricos, na prática, provadores de teoremas pode resolver muitos problemas difíceis, mesmo nessas lógicas indecidíveis.

Problemas relatados

[editar | editar código-fonte]

Um dos problemas é a "verificação da prova", onde uma prova existente para um teorema é válida. Para isso, é geralmente necessário que cada passo individual da prova possa ser verificado por uma função recursiva primitiva ou programa, e portanto o problema é sempre decidível.

Desde que a prova gerada automaticamente seja tipicamente muito extensa, o problema da compressão da prova é crucial e várias táticas e técnicas tentam fazer com que a prova seja a mais sucinta possível.

Assistente de Prova: São necessários usuários humanos capazes de dar dicas de como prosseguir com as provas. Dependendo do grau de automação, um supervisor pode diminuir drasticamente o tamanho da prova.

Outra distinção é às vezes feita entre prova de teoremas de e outras técnicas, onde um processo é considerado prova de teoremas se consiste em uma prova tradicional, começando com os axiomas e produzindo novos passos de inferência utilizando para tal.Outras técnicas podem incluir checagem do modelo,que no caso mais simples, envolve força bruta, manual e enumeração dos muitos estados possíveis (embora a implementação real do modelo requeira muita inteligência, e não simplesmente redução da força bruta e do trabalho manual e/ou artesanal).

Usos na indústria

[editar | editar código-fonte]

O uso comercial de provas dos teoremas automatizados é mais concentrada em projectos de circuito integrado e verificação. Desde o bug do Pentium FDIV, as complicadas unidades de ponto flutuante de microprocessadores modernos foram concebidas com controle extra. Atualmente [vago] AMD, Intel e outros usam a prova automatizada de teoremas para verificar que a divisão e as outras operações são corretamente implementadas em seus processadores.

Provas de teoremas de primeira-ordem

[editar | editar código-fonte]

Provas de teoremas de primeira ordem é um dos campos mais maduros da prova automatizada de teoremas. A lógica é expressiva o suficiente para permitir especificações de problemas arbitrários, muitas vezes em uma forma intuitiva e razoavelmente natural. Por outro lado, ainda semi-decifrável e um número grande de cálculos automatizados já foi desenvolvido, permitindo sistemas totalmente automatizados. Lógicas mais expressivas, como a lógica de ordem superior, permitem a expressão adequada de uma ampla gama de problemas de lógica de primeira ordem, mas a prova de teoremas para estas lógicas é bem menos desenvolvida.

Benchmarks e Competições

[editar | editar código-fonte]

A qualidade dos sistemas implementados foi beneficiada pela existência de uma robusta biblioteca de exemplos de benchmark: "The Thousands of Problems for Theorem Provers (TPTP) Problem Library"[10] — cedidas pela CADE ATP System Competition (CASC), uma competição anual de sistemas de Lógica de primeira ordem para classes importantes de problemas Lógica desse tipo.

Alguns Sistemas importantes (Todos ganharam ao menos uma divisão da competição CASC ) são listadas a seguir:

Técnicas Populares

[editar | editar código-fonte]

See also: Proof assistant#Comparison e Category:Theorem proving software systems

Name License type Web service Library Standalone Version Last update (YYYY-mm-dd format) Author Notice
ACL2 3-clause BSD (em norueguês) (em norueguês) Sim 6.2 2013/06 Matt Kaufmann, J. Strother Moore -
Prover9 / Mace4 GPLv2 (em norueguês) Sim Sim v05 2009/11/04 William McCune / Argonne National Laboratory -
Otter Public Domain Via System on TPTP Sim (em norueguês) 3.3f 2004/09 William McCune / Argonne National Laboratory Succeeded by Prover9 / Mace4
j'Imp ? (em norueguês) (em norueguês) Sim - 2010/05/28 André Platzer -
Metis ? (em norueguês) Sim (em norueguês) 2.2 2010/05/24 Joe Hurd -
Jape ? Sim Sim (em norueguês) 1.0 2010/03/22 Adolfo Gustavo Neto, USP -
PVS ? (em norueguês) Sim (em norueguês) 4.2 2008/07 Computer Science Laboratory of SRI International, California, USA -
Leo II[ligação inativa] ? Via System on TPTP Sim Sim 1.2.8 2011 Christoph Benzmüller, Frank Theiss, Larry Paulson. FU Berlin e University of Cambridge -
EQP ? (em norueguês) Sim (em norueguês) 0.9e 2009/05 William McCune / Argonne National Laboratory -
SAD ? Sim Sim (em norueguês) 2.3-2.5 2008/08/27 Alexander Lyaletski, Konstantin Verchinine, Andrei Paskevich -
PhoX ? (em norueguês) Sim (em norueguês) 0.88.100524 - Christophe Raffalli, Philippe Curmin, Pascal Manoury, Paul Roziere -
KeYmaera GPL Via Java Webstart Sim Sim 2.1 2012/05 André Platzer, Jan-David Quesel; Philipp Rümmer; David Renshaw -
Gandalf ? (em norueguês) Sim (em norueguês) 3.6 2009 Matt Kaufmann e J. Strother Moore, Universidade de Texas em Austin -
Tau ? (em norueguês) Sim (em norueguês) - 2005 Jay R. Halcomb e Randall R. Schulz da H&S Information Systems -
E GPL Via System on TPTP (em norueguês) Sim E 1.4 2011/08/20 Stephan Schulz, Automated Reasoning Group, Technical University of Munich -
SNARK Mozilla Public License (em norueguês) Sim (em norueguês) snark-20080805r018b 2008 Mark E. Stickel -
Vampire ? Via System on TPTP Sim Sim Third re-incarnation Vampire 2011 Andrei Voronkov, Alexandre Riazanov, Krystof Hoder -
Waldmeister ? Sim Sim (em norueguês) - - Thomas Hillenbrand, Bernd Löchner, Arnim Buch, Roland Vogt, Doris Diedrich -
Saturate ? (em norueguês) Sim (em norueguês) 2.5 1996/10 Harald Ganzinger, Robert Nieuwenhuis, Pilar Nivela Pilar Nivela -
Theorem Proving System (TPS) ? (em norueguês) Sim (em norueguês) - 2004/06/24 Carnegie Mellon University -
SPASS ? Sim Sim Sim 3.7 2005/11 Max Planck Institut Informatik -
IsaPlanner GPL (em norueguês) Sim Sim IsaPlanner 2 2007 Lucas Dixon, Johansson Moa -
KeY GPL Sim Sim Sim 1.6 2010/10 Karlsruhe Institute of Technology, Chalmers University of Technology, University of Koblenz -
Theorem Checker ? Sim (em norueguês) (em norueguês) 0 2010 Robert J. Swartz, Northeastern Illinois University -
Princess GPL Via Java Webstart e System on TPTP Sim Sim 2012-11-02 2012 Philipp Rümmer, Uppsala University -

Softwares Livres

[editar | editar código-fonte]

Softwares Privados

[editar | editar código-fonte]

Pessoas Notáveis

[editar | editar código-fonte]

Referências

  1. Frege, Gottlob (1879). Begriffsschrift. [S.l.]: Verlag Louis Neuert 
  2. Frege, Gottlob (1884). Die Grundlagen der Arithmetik (PDF). Breslau: Wilhelm Kobner. Consultado em 27 de setembro de 2013. Arquivado do original (PDF) em 26 de setembro de 2007 
  3. Bertrand Russell; Alfred North Whitehead (1910–1913). Principia Mathematica 1st ed. [S.l.]: Cambridge University Press 
  4. Bertrand Russell; Alfred North Whitehead (1927). Principia Mathematica 2nd ed. [S.l.]: Cambridge University Press 
  5. Herbrand, Jaques (1930). Recherches sur la théorie de la démonstration. [S.l.: s.n.] 
  6. Presburger, Mojżesz (1929). «Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt». Warszawa. Comptes Rendus du I congrès de Mathématiciens des Pays Slaves: 92–101 
  7. a b c d Davis, Martin (2001), «The Early History of Automated Deduction», in: Robinson, Alan; Voronkov, Andrei, Handbook of Automated Reasoning 🔗, 1, Elsevier )
  8. Bibel, Wolfgang (2007). «Early History e Perspectives of Automated Deduction» (PDF). Springer. KI 2007. LNAI (4667): 2–18. Consultado em 2 de setembro de 2012 
  9. Gilmore, Paul (1960). «A proof procedure for quantification theory: its justification e realisation». IBM Journal of Research e Development. 4: 28–35 
  10. Sutcliffe, Geoff. «The TPTP Problem Library for Automated Theorem Proving». Consultado em 8 de setembro de 2012 
  11. «SRI International Computer Science Laboratory - John Rushby». SRI International. Consultado em 22 de setembro de 2012