Prova automática de teoremas

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

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

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. Seu Os Fundamentos da Aritmética, publicado em 1884, 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, e revisado em sua segunda edição em 1927. 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.

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. 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

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". 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.

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.

Decibilidade de um problema

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

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

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 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

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

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" — 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:

• E é um provedor de alta performance totalmente dedicado a lógica de primeira ordem, mas construído em um cálculo equacional puro, desenvolvido primordialmente no grupo de automação de sistemas racionais da Technical University of Munich.
• Otter, desenvolvido no Argonne National Laboratory, é baseado em resolução de primeira ordem e paramodulação. O mesmo desde então tem sido substituído pelo Prover9, que por sua vez é pareado com Mace4.
• SETHEO é um sistema de alta performance baseado em metas diretas de modelos eliminatórios de cálculo. É desenvolvido no grupo de automação de sistemas racionais n a Universidade Técnica de Munique. E e SETHEO tem sidos combinados (com outros sistemas) na composição do provedor de teoremas E-SETHEO.
• Vampire é desenvolvido e implementado na Manchester University por Andrei Voronkov e Krystof Hoder, formalmente também por Alexandre Riazanov. Ele ganhou o CADE ATP System Competition na mais prestigiada categoria: CNF (conjunctive normal form or clausal normal form) por 11 anos (1999, 2001–2010).
• Waldmeister é um sistema especializado para unificação equacional de lógica de primeira ordem. Ele ganhou a categoria CASC (CADE ATP System Competition) nos últimos quatorze anos. (1997–2010).
• SPASS é um teorema lógico de primeira ordem equalizado. Ele é desenvolvido pelo grupo de pesquisas de automação da lógica do Max Planck Institute for Computer Science.

Técnicas Populares

• First-order resolution with unification
• Lean theorem proving
• Model elimination
• Method of analytic tableaux
• Superposition e term rewriting
• Model checking
• Mathematical induction
• Binary decision diagrams
• DPLL
• Higher-order unification

Comparação

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

• Alt-Ergo
• Automath
• CVC
• E
• Gödel-machines
• iProver
• IsaPlanner
• KED theorem prover
• LCF
• LoTREC
• MetaPRL
• NuPRL
• Paradox
• Simplify (GPL'ed since 5/2011)
• Twelf
• SPARK (programming language)

Softwares Privados

• Acumen RuleManager (commercial product)
• ALLIGATOR
• CARINE
• KIV
• Prover Plug-In (commercial proof engine product)
• ProverBox
• ResearchCyc
• Spear modular arithmetic theorem prover

Pessoas Notáveis

• Leo Bachmair, co-developer of the superposition calculus.
• Woody Bledsoe, artificial intelligence pioneer.
• Robert S. Boyer, co-author of the Boyer-Moore theorem prover, co-recipient of the Herbrand Award 1999.
• Alan Bundy, University of Edinburgh, meta-level reasoning for guiding inductive proof, proof planning e recipient of 2007 IJCAI Award for Research Excellence, Herbrand Award, e 2003 Donald E. Walker Distinguished Service Award.
• William McCuneArgonne National Laboratory, author of Otter, the first high-performance theorem prover. Many important papers, recipient of the Herbrand Award 2000.
• Hubert Comon, CNRS e now ENS Cachan. Many important papers.
• Robert Lee Constable, Cornell University. Important contributions to type theory, NuPRL.
• Martin Davis, author of the "Handbook of Artificial Reasoning", co-inventor of the DPLL algorithm, recipient of the Herbrand Award 2005.
• Branden FitelsonUniversity of California at Berkeley. Work in automated discovery of shortest axiomatic bases for logic systems.
• Harald Ganzinger, co-developer of the superposition calculus, head of the MPI Saarbrücken, recipient of the Herbrand Award 2004 (posthumous).
• Michael Genesereth, Stanford University professor of Computer Science.
• Keith Goolsbey chief developer of the Cyc inference engine.
• Michael J. C. Gordon led the development of the HOL theorem prover.
• Gérard Huet Term rewriting, HOL logics, Herbrand Award 1998.
• Robert Kowalski developed the connection graph theorem-prover e SLD resolution, the inference engine that executes logic programs.
• Donald W. LovelandDuke University. Author, co-developer of the DPLL-procedure, developer of model elimination, recipient of the Herbrand Award 2001.
• Norman Megill, developer of Metamath, e maintainer of its site at metamath.org, an online database of automatically verified proofs.
• J Strother Moore, co-author of the Boyer-Moore theorem prover, co-recipient of the Herbrand Award 1999.
• Robert Nieuwenhuis University of Barcelona. Co-developer of the superposition calculus.
• Tobias Nipkow of the Technical University of Munich, contributions to (higher-order) rewriting, co-developer of the Isabelle proof assistant
• Ross Overbeek Argonne National Laboratory. Founder of The Fellowship for Interpretation of Genomes
• Lawrence C. Paulson of the University of Cambridge, work on higher-order logic system, co-developer of the Isabelle Theorem Prover
• David Plaisted University of North Carolina at Chapel Hill. Complexity results, contributions to rewriting e completion, instance-based theorem proving.
• John Rushby Program Director - SRI International
• J. Alan Robinson Syracuse University. Developed original resolution e unification based first order theorem proving, co-editor of the "Handbook of Automated Reasoning", recipient of the Herbrand Award 1996
• Jürgen Schmidhuber Work on Gödel Machines: Self-Referential Universal Problem Solvers Making Provably Optimal Self-Improvements
• Stephan Schulz, E theorem Prover.
• Natarajan Shankar SRI International, work on decision procedures, little engines of proof, co-developer of PVS.
• Mark Stickel SRI International. Recipient of the Herbrand Award 2002.
• Geoff Sutcliffe University of Miami. Maintainer of the TPTP collection, an organizer of the CADE annual contest.
• Dolph UlrichPurdue, Work on automated discovery of shortest axiomatic bases for systems.
• Robert VeroffUniversity of New Mexico. Many important papers.
• Andrei VoronkovDeveloper of Vampire e Co-Editor of the "Handbook of Automated Reasoning"
• Larry WosArgonne National Laboratory. (Otter) Many important papers. Very first Herbrand Award winner (1992)
• Wen-Tsun Wu Work in geometric theorem proving: Wu's method, Herbrand Award 1997
• Christoph Weidenbach, author of SPASS, automated theorem prover.

Ver também

• Symbolic computation
• Computer-aided proof
• Automated reasoning
• Formal verification
• Logic programming
• Proof checking
• Model checking
• Proof complexity
• Computer algebra system
• Program analysis (computer science)
• General Problem Solver
• Metamath - a language for developing strictly formalized mathematical definitions e proofs accompanied by a proof checker for this language e a growing database of thousands of proved theorems; while the Metamath language is not accompanied with an automated theorem prover, it can be regarded as important because the formal language behind it allows development of such a softwarePredefinição:Why?; as of March, 2012, there is no "widely" known such software, so it is not a subject of "automated theorem proving" (it can become such a subject Predefinição:Why?), but it is a proof assistant.^{[carece de fontes]}

Referências

• Chin-Liang Chang; Richard Char-Tung Lee (1973). Symbolic Logic e Mechanical Theorem Proving. [S.l.]: Academic Press 
• Loveland, Donald W. (1978). Automated Theorem Proving: A Logical Basis. Fundamental Studies in Computer Science Volume 6. [S.l.]: North-Holland Publishing 
• Gallier, Jean H. (1986). Logic for Computer Science: Foundations of Automatic Theorem Proving. [S.l.]: Harper & Row Publishers (Available for free download) 
• Duffy, David A. (1991). Principles of Automated Theorem Proving. [S.l.]: John Wiley & Sons 
• Wos, Larry; Overbeek, Ross; Lusk, Ewing; Boyle, Jim (1992). Automated Reasoning: Introduction e Applications 2nd ed. [S.l.]: McGraw-Hill 
• Alan Robinson e Andrei Voronkov (eds.), ed. (2001). Handbook of Automated Reasoning Volume I & II. [S.l.]: Elsevier e MIT Press 
• Fitting, Melvin (1996). First-Order Logic e Automated Theorem Proving 2nd ed. [S.l.]: Springer