Prova automática de teoremas

Origem: Wikipédia, a enciclopédia livre.
Ir para: navegação, pesquisa
Trecho de uma prova em agda2

Prova automática de teoremas (PAT) ou dedução automática é 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 raizes da lógica formal vem de Aristotle, o final do século 19 e no começo do século 20 Aconteceu o desenvolvimento da logica moderna e da matemátia formal.Frege's Begriffsschrift (1879) introduziu tanto a logica proposicional como o que é essencialmente a lógica de predicados moderna.[1] His Foundations of Arithmetic, publicado em 1884,[2] expressedexpressam (partes da) matematica 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. In 1920, Thoralf Skolem simplificou um resultado anterior de Leopold Löwenheim,lavando 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 formulas da lógica de primeira ordem (e portanto, avalidade 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 chamdo deAritimética de Presburger em sua honra) é [[|decidabilidade|Decidability (logic)]] e deu um algoritmo que pode determinar se uma sentença dada neta linguagem era verdadeira ou false.[6] [7] Entretanto, pouco tempo após esse reultado positivo, Kurt Gödel publicou On Formally Undecidable Propositions of Principia Mathematica e Related Systems (1931), mostrando que em todo sistema axiomatico fortemente baseado existem sentenças que são verdadeiras e que nao 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 a´pós a Segunda Guerra Mundial, o primeiro genereal 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ácupo 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 deducao matematica para a logica proposicional de Principia Mathematica, desenvolvido porAllen Newell, Herbert A. Simon e J. C. Shaw.Este também rodava em um JOHANNIAC, the 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, substituicao de variaveis proposicionais, e a substituição de dormulas por suas definições. O sistema usava orientação heurística, e tentaThe system used heuristic guidance, e 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 raciocienio humano, e nao conseguia garantir que uma prova podia ser encontrada para cada teorema válido a priori. Em contraste, outro, mas algoritmos mais sitematicos alcançaram, pelo menos teoricamente, Inconpletude para a lgica 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 proposicional 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 prigrama de Gilmore usou conversao para forma normal disjuntiva, uma forma onde a satisfabilidade da formula é óbvia.[7] [9]

Decibilidadae de um problema[editar | editar código-fonte]

Predefinição:Unreferenced section Dependendo da lógica subjacente, o problema de decidir a validade de uma fórmula varia do trivial ao impossível. Para o caso frequente da lógica proposicional, o problema é decidivel, porém Co-NP-complete,acredita-se que existam apenas algoritmos em tempo exponencial para tarefas de prova. Para a first order predicate calculus, com n~enum ("proper") axioma, teorema da incmpletude de Gödel afirma que qualquer formula válida pode ser comprovada.

Entretanto, formulas invalidas não podem sempre serem reconhecias. além disso, uma teoria formal consistente que contem logica de primeira ordem dos numeros naturais(contendo alguns "axiomas adequados"), por [[Teorema de incompletude de Gödel], contem sentenças verdadeiras que nao podem ser provadas. Nestes casos, uma prova automatizada do teorema pode vir a falhar, pois poderá a 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 necessario que cada passo individual da prova possa ser verificado por uma funcao recursiva primitiva ou programa, e portanto o problema é sempre decidivel.

Desde que a prova gerada automaticamente são tipicamente muito extensas, o problema da compressao da prova é crucial e várias técticas tentam fazer co 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 regras de inferência.Outras técnicas podem incluir checagem do modeloque, no caso mais simples, envolve força bruta enumeração dos muitos estados possíveis (embora a implementação real de damas modelo requer muita inteligência, e não simplesmente reduzir a força bruta).

Usos na indústria[editar | editar código-fonte]

O uso comercial de prova de teoremas automatizada é mais concentrada em [[designs de circuito integrado ] e verificação. Desde o bug do Pentium FDIV, a complicada unidade de ponto flutuante s de microprocessadores modernos foram concebidos com controle extra. Hoje em dia[quando?] 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 First-order é um dos campos mais maduros da prova automatizada de teoremas. A lógica é expressiva o suficiente para permitir especificações de problemas arbitrarios, muitas vezes em uma forma intuitiva e razoavelmente natural. Por outro lado, ainda semi-decifravel e um numero grande de calculos automatizados ja foi desenvolvido, permitinso 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 eCompetições[editar | editar código-fonte]

A qualidade dos sistemas implementados foi beneficiada pela existencia de umarobusta 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 logica de primeira ordem para classes importantes de problemas logica de primeira ordem.

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

Técnicas Populares[editar | editar código-fonte]

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

Softwares Livres[editar | editar código-fonte]

Sofwares Privados[editar | editar código-fonte]

Pessoas Notáveis[editar | editar código-fonte]

See also[editar | editar código-fonte]

Notes[editar | editar código-fonte]

  1. Frege, Gottlob. Begriffsschrift. [S.l.]: Verlag Louis Neuert, 1879.
  2. Frege, Gottlob. Die Grundlagen der Arithmetik. Breslau: Wilhelm Kobner, 1884.
  3. Bertrand Russell; Alfred North Whitehead. Principia Mathematica. 1st ed. [S.l.]: Cambridge University Press, 1910-1913.
  4. Bertrand Russell; Alfred North Whitehead. Principia Mathematica. 2nd ed. [S.l.]: Cambridge University Press, 1927.
  5. Herbrand, Jaques. Recherches sur la théorie de la démonstration. [S.l.: s.n.], 1930.
  6. 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: 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, http://cs.nyu.edu/cs/faculty/davism/early.ps )
  8. Bibel, Wolfgang. (2007). "Early History e Perspectives of Automated Deduction". KI 2007 (4667): 2–18. Springer.
  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. Página visitada em 8 September 2012.
  11. SRI International Computer Science Laboratory - John Rushby. SRI International. Página visitada em 22 September 2012.

References[editar | editar código-fonte]


Aviso: A chave de ordenação padrão "Prova Automatica Teoremas" sobrepõe-se à anterior "Automated Theorem Proving".