Em ciência da computação, particularmente em representação do conhecimento e raciocínio e metalógica, a área de raciocínio automatizado dedica-se a compreender diferentes aspectos do raciocínio. O estudo do raciocínio automatizado ajuda a produzir programas de computador que permitem que computadores raciocinem completa, ou quase completamente, de forma automática. Embora o raciocínio automatizado seja considerado um subcampo da inteligência artificial, também possui 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 demonstração automatizada de teoremas (e o subcampo menos automatizado, porém mais pragmático, da demonstração interativa de teoremas) e a verificação automatizada de provas (vista como raciocínio garantidamente correto sob premissas fixas). Trabalho extensivo também foi realizado em raciocínio por analogia usando indução e abdução.Defourneaux, Gilles, and Nicolas Peltier. "Analogy and abduction in automated deduction." IJCAI (1). 1997.
Outros tópicos importantes incluem o raciocínio sob incerteza e o raciocínio não monotônico. Uma parte importante do campo da incerteza é a argumentação, onde restrições adicionais de minimalidade e consistência são aplicadas sobre a dedução automática mais padrão. O sistema OSCAR de John Pollock é um exemplo de sistema de argumentação automatizado que é mais específico do que ser apenas um provador automatizado de teoremas.
Ferramentas e técnicas de raciocínio automatizado incluem as lógicas e cálculos clássicos, lógica fuzzy, inferência bayesiana, raciocínio com entropia máxima e muitas técnicas ad hoc menos formais.
Na década de 2020, para melhorar a capacidade dos modelos de linguagem de grande escala de resolver problemas complexos, pesquisadores de IA criaram modelos de linguagem de raciocínio que podem gastar mais tempo no problema antes de gerar uma resposta e arquiteturas neuro-simbólicas que usam sistemas de raciocínio simbólicos para prevenir alucinações.
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 na qual cada 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.C. Hales, Thomas "Formal Proof", University of Pittsburgh. Retrieved on 2010-10-19
Alguns consideram o encontro de verão de Cornell em 1957, que reuniu muitos lógicos e cientistas da computação, como a origem do raciocínio automatizado, ou da dedução automatizada."Automated Deduction (AD)", [The Nature of PRL Project]. Retrieved on 2010-10-19 Outros dizem que começou antes disso com o programa Logic Theorist de 1955 de Newell, Shaw e Simon, ou com a implementação de 1954 por Martin Davis do procedimento de decisão de Presburger (que provou que a soma de dois números pares é par). Here: p.15
O raciocínio automatizado, embora uma área de pesquisa significativa e popular, passou por um "inverno da IA" nos anos oitenta e início dos anos noventa. O campo subsequentemente se recuperou, no entanto. Por exemplo, em 2005, a Microsoft começou a usar tecnologia de verificação em muitos de seus projetos internos e planeja incluir uma linguagem de especificação e verificação lógica em sua versão de 2012 do Visual C.
Contribuições significativas Principia Mathematica foi um trabalho marcante na lógica formal escrito por Alfred North Whitehead e Bertrand Russell. Seu propósito era derivar todas ou algumas das expressões matemáticas, em termos de lógica simbólica. Principia Mathematica foi inicialmente publicada em três volumes em 1910, 1912 e 1913."Principia Mathematica", at Stanford University. Retrieved 2010-10-19 Sucedeu The Principles of Mathematics, um livro de 1903 de Bertrand Russell, no qual Russell apresentou seu famoso paradoxo e argumentou sua tese de que matemática e lógica são idênticas.
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" na demonstração de teoremas e foi demonstrado em cinquenta e dois teoremas do capítulo dois do Principia Mathematica, provando trinta e oito deles."The Logic Theorist and its Children" . Retrieved 2010-10-18 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. Após uma tentativa frustrada de publicar seus resultados, Newell, Shaw e Herbert relataram em sua publicação de 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 aumentará rapidamente até que (num futuro visível) a gama de problemas que elas podem resolver seja tão extensa quanto aquela à qual a mente humana tem sido aplicada."Shankar, Natarajan Little Engines of Proof, Computer Science Laboratory, SRI International. Retrieved 2010-10-19
Exemplos de Provas Formais
{| class="wikitable" |- ! 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 do Cálculo || HOL Light || Harrison || Henstock |- | 2000 || Fundamental da Álgebra || Mizar || Milewski || Brynski |- | 2000 || Fundamental da Álgebra || Rocq (então: Coq) || Geuvers et al. || Kneser |- | 2004 || Quatro Cores || Rocq (então: Coq) || Gonthier || Robertson et al. |- | 2004 || Números Primos || Isabelle|| Avigad et al. || Selberg-Erdős |- | 2005 || Curva de Jordan || HOL Light || Hales || Thomassen |- | 2005 || Ponto Fixo de Brouwer || HOL Light || Harrison || Kuhn |- | 2006 || Flyspeck 1 || Isabelle|| Bauer–Nipkow || Hales |- | 2007 || Resíduo de Cauchy || HOL Light || Harrison || Clássica |- | 2008 || Números Primos || HOL Light || Harrison || Prova analítica |- | 2012 || Feit–Thompson || Rocq (então: Coq) || Gonthier et al. || Bender, Glauberman and Peterfalvi |- | 2016 || Problema dos triplos pitagóricos booleanos || Formalizado como SAT || Heule et al. || Nenhuma
Sistemas de prova Provador de Teoremas Boyer-Moore (NQTHM) O design do NQTHM foi influenciado por John McCarthy e Woody Bledsoe. Iniciado em 1971 em Edimburgo, Escócia, este foi um provador de teoremas totalmente automático construído usando Lisp puro. Os principais aspectos do NQTHM foram: o uso de Lisp como uma lógica de trabalho. a dependência de um princípio de definição para funções recursivas totais. o uso extensivo de reescrita e "avaliação simbólica". uma heurística de indução baseada na falha da avaliação simbólica.The Boyer-Moore Theorem Prover Retrieved on 2010-10-23Boyer, Robert S. and Moore, J Strother and Passmore, Grant Olney The PLTP Archive. Retrieved on 2023-07-27
HOL Light Escrito em OCaml, o HOL Light é projetado para ter uma base lógica simples e limpa e uma implementação desobstruída. É essencialmente outro assistente de prova para lógica clássica de ordem superior.Harrison, John HOL Light: an overview. Retrieved 2010-10-23
Rocq Desenvolvido na França, o Rocq é outro assistente de prova automatizado, que pode extrair automaticamente programas executáveis a partir de especificações, como código-fonte Objective CAML ou Haskell. Propriedades, programas e provas são formalizados na mesma linguagem chamada Cálculo das Construções Indutivas (CIC).Introduction to Coq. Retrieved 2010-10-23
Aplicações
O raciocínio automatizado tem sido mais comumente usado para construir provadores automatizados de teoremas. Frequentemente, no entanto, os provadores de teoremas exigem alguma orientação humana para serem eficazes e, portanto, se qualificam mais geralmente como assistentes de prova. Em alguns casos, tais provadores criaram novas abordagens para provar um teorema. O Logic Theorist é um bom exemplo disso. O programa criou 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 de tais problemas que é atualizada regularmente. Há também uma competição entre provadores automatizados de teoremas realizada regularmente na conferência CADE (Pelletier, Sutcliffe and Suttner 2002); os problemas para a competição são selecionados da biblioteca TPTP.
Ver também Aprendizado de máquina automatizado (AutoML) Demonstração automatizada de teoremas Raciocinador semântico Análise de programas (ciência da computação) Aplicações da inteligência artificial Esboço da inteligência artificial Casuística • Raciocínio baseado em casos Raciocínio abdutivo Mecanismo de inferência Raciocínio de senso comum
Conferências e workshops International Joint Conference on Automated Reasoning (IJCAR) Conference on Automated Deduction (CADE)
Periódicos Journal of Automated Reasoning
Comunidades Association for Automated Reasoning (AAR)
Referências
Ligações externas International Workshop on the Implementation of Logics Workshop Series on Empirically Successful Topics in Automated Reasoning Categoria:Inteligência artificial Categoria:Ciência da computação Categoria:Ciência da computação teórica Categoria:Aprendizagem de máquina