Raciocínio automatizado - Automated reasoning

Na ciência da computação , em particular na representação e raciocínio do conhecimento e na metalógica , a área do raciocínio automatizado se dedica à compreensão de diferentes aspectos do raciocínio . O estudo do raciocínio automatizado ajuda a produzir programas de computador que permitem aos computadores raciocinar completamente, ou quase completamente, automaticamente. Embora o raciocínio automatizado seja considerado um subcampo da inteligência artificial , ele também tem conexões com a ciência da computação teórica e a filosofia .

As subáreas mais desenvolvidas do raciocínio automatizado são a prova automatizada de teoremas (e o subcampo menos automatizado, porém mais pragmático da prova interativa de teoremas ) e verificação de prova automatizada (vista como raciocínio correto garantido sob suposições fixas). Um extenso trabalho também foi feito no raciocínio por analogia usando indução e abdução .

Outros tópicos importantes incluem raciocínio sob incerteza e raciocínio não monotônico . Uma parte importante do campo da incerteza é a da argumentação, onde outras restrições de minimalidade e consistência são aplicadas em cima da dedução automatizada mais padrão. O sistema OSCAR de John Pollock é um exemplo de sistema de argumentação automatizado que é mais específico do que apenas um provador automatizado de teoremas.

Ferramentas e técnicas de raciocínio automatizado incluem a lógica clássica e cálculos, lógica fuzzy , inferência Bayesiana , raciocínio com entropia máxima e muitas técnicas ad hoc menos formais .

Primeiros anos

O desenvolvimento da lógica formal desempenhou um grande papel no campo do raciocínio automatizado, que por sua vez levou ao desenvolvimento da inteligência artificial . Uma prova formal é uma prova em que toda inferência lógica foi verificada até os axiomas fundamentais da matemática. Todas as etapas lógicas intermediárias são fornecidas, sem exceção. Nenhum apelo é feito à intuição, mesmo que a tradução da intuição para a lógica seja rotineira. Assim, uma prova formal é menos intuitiva e menos suscetível a erros lógicos.

Alguns consideram a reunião de verão de Cornell de 1957, que reuniu muitos lógicos e cientistas da computação, como a origem do raciocínio automatizado ou dedução automatizada . Outros dizem que começou antes disso, com o programa Logic Theorist de Newell, Shaw e Simon de 1955 , ou com a implementação de Martin Davis em 1954 do procedimento de decisão de Presburger (que provou que a soma de dois números pares é par).

O raciocínio automatizado, embora uma área significativa e popular de pesquisa, passou por um " inverno da IA " nos anos oitenta e início dos anos noventa. O campo posteriormente reviveu, no entanto. Por exemplo, em 2005, a Microsoft começou a usar tecnologia de verificação em muitos de seus projetos internos e está planejando incluir uma especificação lógica e linguagem de verificação em sua versão 2012 do Visual C.

Contribuições significativas

Principia Mathematica foi um marco na lógica formal escrito por Alfred North Whitehead e Bertrand Russell . Principia Mathematica - também significando Princípios da Matemática - foi escrito com o propósito de derivar todas ou algumas das expressões matemáticas , em termos de lógica simbólica . Principia Mathematica foi publicado inicialmente em três volumes em 1910, 1912 e 1913.

Logic Theorist (LT) foi o primeiro programa desenvolvido em 1956 por Allen Newell , Cliff Shaw e Herbert A. Simon para "imitar o raciocínio humano" ao provar teoremas e foi demonstrado em cinquenta e dois teoremas do capítulo dois do Principia Mathematica, provando trinta -oito deles. Além de provar os teoremas, o programa encontrou uma prova para um dos teoremas que era mais elegante do que a fornecida por Whitehead e Russell. Depois de uma tentativa malsucedida de publicar seus resultados, Newell, Shaw e Herbert relataram em sua publicação em 1958, The Next Advance in Operation Research :

“Existem agora no mundo máquinas que pensam, que aprendem e que criam. Além disso, sua capacidade de fazer essas coisas vai aumentar rapidamente até (em um futuro visível) a gama de problemas que podem lidar será extensiva com a gama a que a mente humana foi aplicada. "

Exemplos de provas formais

Ano Teorema Sistema de Prova Formalizador Prova Tradicional
1986 Primeira Incompletude Boyer-Moore Shankar Gödel
1990 Reciprocidade Quadrática Boyer-Moore Russinoff Eisenstein
1996 Fundamental - de Cálculo HOL Light Harrison Henstock
2000 Fundamental - de Álgebra Mizar Milewski Brynski
2000 Fundamental - de Álgebra Coq Geuvers et al. Kneser
2004 Quatro cores Coq Gonthier Robertson et al.
2004 Número primo Isabelle Avigad et al. Selberg - Erdős
2005 Jordan Curve HOL Light Hales Thomassen
2005 Ponto Fixo Brouwer HOL Light Harrison Kuhn
2006 Flyspeck 1 Isabelle Bauer- Nipkow Hales
2007 Resíduo Cauchy HOL Light Harrison Clássico
2008 Número primo HOL Light Harrison Prova analítica
2012 Feit-Thompson Coq Gonthier et al. Bender, Glauberman e Peterfalvi
2016 Problema dos triplos booleanos pitagóricos Formalizado como SAT Heule et al. Nenhum

Sistemas de prova

Provador do Teorema de Boyer-Moore (NQTHM)
O design do NQTHM foi influenciado por John McCarthy e Woody Bledsoe. Iniciado em 1971 em Edimburgo, Escócia, este era um provador de teoremas totalmente automático construído usando Pure Lisp . Os principais aspectos do NQTHM foram:
  1. o uso do Lisp como lógica de trabalho.
  2. a confiança em um princípio de definição para funções recursivas totais.
  3. o uso extensivo de reescrita e "avaliação simbólica".
  4. uma heurística de indução baseava o fracasso da avaliação simbólica.
HOL Light
Escrito em OCaml , o HOL Light foi projetado para ter uma base lógica simples e limpa e uma implementação organizada. É essencialmente outro assistente de prova para a lógica clássica de ordem superior.
Coq
Desenvolvido na França, Coq é outro assistente de prova automatizado, que pode extrair automaticamente programas executáveis ​​de especificações, como código-fonte Objective CAML ou Haskell . Propriedades, programas e provas são formalizados na mesma linguagem chamada Cálculo de Construções Indutivas (CIC).

Formulários

O raciocínio automatizado tem sido mais comumente usado para construir provadores automatizados de teoremas. Freqüentemente, no entanto, os provadores de teoremas requerem alguma orientação humana para serem eficazes e, portanto, geralmente são qualificados como assistentes de prova . Em alguns casos, esses provadores surgiram com novas abordagens para provar um teorema. O Logic Theorist é um bom exemplo disso. O programa apresentou uma prova para um dos teoremas do Principia Mathematica que era mais eficiente (exigindo menos etapas) do que a prova fornecida por Whitehead e Russell. Programas de raciocínio automatizado estão sendo aplicados para resolver um número crescente de problemas em lógica formal, matemática e ciência da computação, programação lógica , verificação de software e hardware, projeto de circuitos e muitos outros. O TPTP (Sutcliffe e Suttner 1998) é uma biblioteca desses problemas que é atualizada regularmente. Também há uma competição entre provadores de teoremas automatizados realizada regularmente na conferência do CADE (Pelletier, Sutcliffe e Suttner 2002); os problemas para a competição são selecionados da biblioteca TPTP.

Veja também

Conferências e workshops

Diários

Comunidades

Referências

  1. ^ Defourneaux, Gilles e Nicolas Peltier. " Analogia e abdução na dedução automática ." IJCAI (1). 1997.
  2. ^ John L. Pollock
  3. ^ C. Hales, Thomas "Formal Proof" , University of Pittsburgh. Obtido em 19/10/2010
  4. ^ a b "Dedução automatizada (AD)" , [The Nature of PRL Project] . Obtido em 19/10/2010
  5. ^ Martin Davis (1983). "A pré-história e a história inicial da dedução automatizada". Em Jörg Siekmann; G. Wrightson (eds.). Automation of Reasoning (1) - Classical Papers on Computational Logic 1957–1966 . Heidelberg: Springer. pp. 1-28. ISBN 978-3-642-81954-4. Aqui: pág. 15
  6. ^ "Principia Mathematica" , na Universidade de Stanford . Recuperado em 19/10/2010
  7. ^ "The Logic Theorist and its Children" . Recuperado em 18/10/2010
  8. ^ Shankar, Natarajan Pequenos motores da prova , laboratório de ciência da computação, SRI International . Recuperado em 19/10/2010
  9. ^ Shankar, N. (1994), Metamathematics, Machines, and Gödel's Proof , Cambridge, Reino Unido: Cambridge University Press, ISBN 9780521585330
  10. ^ Russinoff, David M. (1992), "A Mechanical Proof of Quadratic Reciprocity", J. Autom. Razão. , 8 (1): 3-21, doi : 10.1007 / BF00263446
  11. ^ Gonthier, G .; et al. (2013), "A Machine-Checked Proof of the Odd Order Theorem" (PDF) , em Blazy, S .; Paulin-Mohring, C .; Pichardie, D. (eds.), Interactive Theorem Proving , Lecture Notes in Computer Science, 7998 , pp. 163-179, doi : 10.1007 / 978-3-642-39634-2_14 , ISBN 978-3-642-39633-5
  12. ^ Heule, Marijn JH ; Kullmann, Oliver; Marek, Victor W. (2016). "Resolvendo e verificando o problema dos triplos pitagóricos booleanos via cubo e conquista". Teoria e aplicações de testes de satisfação - SAT 2016 . Notas de aula em Ciência da Computação. 9710 . pp. 228–245. arXiv : 1605,00723 . doi : 10.1007 / 978-3-319-40970-2_15 . ISBN 978-3-319-40969-6.
  13. ^ O provador do teorema de Boyer- Moore . Obtido em 23/10/2010
  14. ^ Harrison, John HOL Light: uma vista geral . Recuperado em 23/10/2010
  15. ^ Introdução ao Coq . Recuperado em 23/10/2010
  16. ^ Automated Reasoning , Stanford Encyclopedia . Recuperado 2010-10-10

links externos