# Logic Theorist

Logic Theorist é um programa de computador escrito em 1955 e 1956 por Allen Newell, Herbert Simon e J. C. Shaw. Foi o primeiro programa deliberadamente projetado para imitar as habilidades de resolver problemas de um ser humano e é chamado, por alguns, de "o primeiro programa de inteligência artificial", embora alguns considerem o programa do jogo de damas de Arthur Samuel anterior. Christopher Strachey também escreveu um programa de damas em 1951. Este programa foi concebido para demonstrar teoremas do cálculo proposicional. Ele acabaria por se demonstrar 38 dos primeiros 52 teoremas do Principia Mathematica de Russell e de Whitehead, e encontrar provas novas e mais elegantes de alguns.

## História

Em 1955, quando Newell e Simon começaram a trabalhar na Lógica Teórica, o campo de inteligência artificial ainda não existia. Mesmo o termo em si ("inteligência artificial") não seria cunhado até o verão seguinte (O termo "inteligência artificial" foi cunhado por John McCarthy na proposta para a Conferência de Dartmouth de 1956. A conferência é "geralmente reconhecida como a data de nascimento oficial da nova ciência.").
Herbert Simon foi um cientista político por formação e já tinha produzido um trabalho clássico no estudo de como burocracias funcionavam, bem como desenvolveu sua teoria de racionalidade limitada (pela qual mais tarde viria a ganhar um Prêmio Nobel). O estudo das organizações empresariais pode parecer, superficialmente, muito diferente da inteligência artificial, mas exige a mesma percepção sobre a natureza humana de resolução de problemas e tomada de decisões. Simon lembra de estar prestando uma consultoria na RAND no início dos anos 1950 e vendo uma impressora digitando um mapa, com letras simples e pontuação como símbolos. Ele percebeu que uma máquina que pudesse manipular símbolos poderia assim também simular a tomada de decisões e, eventualmente, simular mesmo o processo do pensamento humano.
O programa que imprimia o mapa tinha sido escrito por Alan Newell, um cientista da RAND Corporation, estudando a logística e teoria da organização. Para Newell, o momento decisivo tinha sido em 1954, quando Oliver Selfridge chegou à RAND para descrever seu trabalho em pattern matching. Assistindo a apresentação, Newell de repente compreendeu como a interação de unidades programáveis simples poderiam realizar comportamentos complexos, incluindo o comportamento inteligente dos seres humanos. "Tudo aconteceu em uma tarde", ele diria mais tarde. Foi um raro momento de epifania científica.
   Eu tive uma sensação de claridade de que se tratava de um novo caminho, e que eu estava a ir para baixo. Eu não tinha tido essa sensação muitas vezes. Eu sou muito cético, e assim eu normalmente não sairia em um apito, mas nessa vez eu saí. Completamente absorvido na mesma, sem existir em dois ou três níveis de consciência no qual você está trabalhando, e ciente de que você está trabalhando, e consciente das conseqüências e implicações, o modo normal do pensamento. Não. Ccompletamente absorvido por 10-12 horas.
Newell e Simon começaram a falar sobre a possibilidade de ensinar máquinas a pensar. O primeiro projeto foi um programa que pudesse provar teoremas matemáticos, como os usados em Bertrand Russell e Alfred North Whitehead Principia Mathematica. Eles pediram a ajuda do programador de computador J. C. Shaw, também da RAND, para desenvolver o programa. (Newell diz: "Cliff foi o genuíno cientista da computação dos três".
A primeira versão foi simulada a mão: eles escreveram o programa em cartões 3x5 e, como lembrou Simon:
   Em janeiro de 1956, agregamos a minha esposa e três filhos, juntamente com alguns alunos de pós-graduação. Para cada membro do grupo, demos um dos cartões, de modo que cada um se tornou, de fato, um componente do programa de computador ... Aqui foi a natureza imitando a arte imitando a natureza.
Eles conseguiram demonstrar que o programa poderia demonstrar teoremas, tanto quanto um matemático talentoso. Eventualmente Shaw foi capaz de executar o programa no computador em um RAND nas instalações da Santa Monica.
No verão de 1956, John McCarthy, Marvin Minsky, Claude Shannon e Nathaniel Rochester organizaram uma conferência sobre o assunto do que eles chamavam de "inteligência artificial" (um termo cunhado por McCarthy para a ocasião). Newell e Simon orgulhosamente apresentaram para o grupo o Logic Theorist e fcaram um pouco surpresos quando o programa teve uma recepção morna. Pamela McCorduck escreve que: "a evidência é que ninguém impediu Newell e Simon de perceber a importância de longo alcance do que estavam fazendo." Simon confessou que "foram provavelmente bastante arrogante sobre tudo" e adicionou:
   Eles não queriam nos ouvir, e temos certeza que não queríamos ouvir nada deles: nós tínhamos alguma coisa para mostrar-los! ... De certa forma, foi irônico, pois já tinha feito o primeiro exemplo de que eles estavam atrás e, segundo, eles não prestaram muita atenção a ele.
O Logic Theorist logo provou 38 dos primeiros 52 teoremas do capítulo 2 do Principia Mathematica. A prova do Teorema 2.85 era realmente mais elegante do que a prova produzida laboriosamente à mão por Russell e Whitehead. Simon foi capaz de mostrar a nova prova para Bertrand Russell que "respondeu com deleite." Eles tentaram publicar a nova prova no The Journal of Symbolic Logic, mas o artigo foi rejeitado pelo argumento de que uma nova prova de um teorema matemático elementar não era notável, aparentemente esquecendo que um dos autores era um programa de computador.
Newell e Simon formaram uma parceria duradoura, fundando um dos primeiros laboratórios de IA em Carnegie Tech e desenvolvendo uma série de influentes programas de inteligência artificial e idéias, incluindo o GPS, Soar e sua teoria unificada da cognição.

## A influência do Logic Theorist na IA

O Logic Theorist introduziu diversos conceitos que seriam essenciais para a pesquisa em IA:

### Raciocínio como pesquisa

    o Logic Theorist explorou uma árvore de busca: a raiz era a primeira hipótese, cada ramo era uma dedução com base nas regras da lógica. Em algum lugar "acima" na árvore estava o objetivo: a proposição que o programa destinava-se a provar. O percurso ao longo dos ramos que levava ao gol era uma prova - uma série de afirmações, cada uma deduzida usando-se as regras da lógica, que levavam da hipótese à proposição a ser provada.

### Heurística

    Newell e Simon compreenderam que a busca em árvore cresceria exponencialmente e que eles precisavam "cortar" alguns ramos, com "regras de ouro" para determinar quais as vias não eram susceptíveis de conduzir a uma solução. Chamaram a estas regras ad-hoc "heurísticas", usando um termo introduzido por George Polya em seu livro clássico sobre prova matemática, How to Solve It (como resolvê-lo) (Alan Newell teve cursos de Polya em Stanford). Heurística se tornaria uma importante área de pesquisa em inteligência artificial e continua a ser um importante método para superar a intratável explosão combinatória de buscas em crescimento exponencial.

### Processamento de Lista

    Para implementar o Logic Theorist em um computador, os três pesquisadores desenvolveram uma linguagem de programação IPL, onde utilizaram a mesma forma de processamento de listas simbólicas que viria a constituir a base da linguagem de programação Lisp de John McCarthy, uma loinguagem importante ainda usada por pesquisadores de IA$^{pp.6–48}$$^{pp.167–168}$.

## Implicações filosóficas

Pamela McCorduck escreve que o Logic Theorist era "prova positiva de que uma máquina pode executar tarefas até aqui consideradas inteligentes, criativas e exclusivas dos humanos"$^{pp.167}$. E, como tal, representa um marco no desenvolvimento da inteligência artificial e a nossa compreensão da inteligência em geral.
Simon famosamente disse a uma classe de pós-graduação em janeiro de 1956, "No Natal, Al Newell e eu inventamos uma máquina de pensar"$^{pp.138}$, e ia escrever:
   [Nós] inventamos um programa de computador capaz de pensar não-numericamente, , assim, resolvemos o venerável problema corpo-mente, explicando como o sistema composto por matéria pode ter as propriedades da mente.
Esta declaração, que as máquinas podem ter mentes assim como as pessoas, seria mais tarde denominada "IA Forte" pelo filósofo John Searle. Continua a ser um assunto de sério debate até os dias atuais.
Pamela McCorduck, também vê no Logic Theorist a estréia de uma nova teoria da mente, o modelo do processamento da informação (às vezes chamado computacionalismo). Ela escreve que "esta visão viria a ser fundamental para seu trabalho posterior, e em sua opinião, fundamental para compreender a mente no século XX, como o princípio da seleção natural de Darwin tinha sido para a compreensão da biologia do século XIX"$^{pp.127}$. Newell e Simon viriam a formalizar esta proposta como a hipótese dos sistemas de símbolos físicos.