# Lógica na ciência da computação

A lógica na ciência da computação cobre a sobreposição entre o campo da lógica e o da ciência da computação. O tema pode ser essencialmente dividido em três áreas principais:
* Fundamentos teóricos e análise
* Uso de tecnologia de computador para ajudar os lógicos
* Uso de conceitos da lógica para aplicativos de computador

## Fundamentos teóricos e análise

A lógica desempenha um papel fundamental na ciência da computação. Algumas das principais áreas da lógica que são particularmente significativas são a teoria da computabilidade (anteriormente chamada de teoria da recursão), a lógica modal e a teoria das categorias . A teoria da computação é baseada em conceitos definidos por lógicos e matemáticos como Alonzo Church e Alan Turing . Church mostrou pela primeira vez a existência de problemas algoritmicamente insolúveis usando sua noção de definibilidade lambda. Turing deu a primeira análise convincente do que pode ser chamado de procedimento mecânico e Kurt Gödel afirmou que achou a análise de Turing "perfeita". Além disso, algumas outras áreas importantes de sobreposição teórica entre lógica e ciência da computação são:
* O teorema da incompletude de Gödel prova que qualquer sistema lógico poderoso o suficiente para caracterizar a aritmética conterá afirmações que não podem ser provadas nem refutadas dentro desse sistema. Isso tem aplicação direta a questões teóricas relacionadas à viabilidade de provar a completude e correção do software.
* O problema do quadro é um problema básico que deve ser superado ao usar a lógica de primeira ordem para representar os objetivos e o estado de um agente de inteligência artificial.
* A correspondência Curry-Howard é uma relação entre sistemas lógicos e software. Essa teoria estabeleceu uma correspondência precisa entre provas e programas. Em particular, mostrou que os termos no cálculo lambda simplesmente tipado correspondem a provas da lógica proposicional intuicionista.
* A teoria das categorias representa uma visão da matemática que enfatiza as relações entre as estruturas. Está intimamente ligado a muitos aspectos da ciência da computação: sistemas de tipos para linguagens de programação, teoria dos sistemas de transição, modelos de linguagens de programação e teoria da semântica das linguagens de programação.

## Computadores para ajudar os lógicos

Uma das primeiras aplicações a usar o termo inteligência artificial foi o sistema Logic Theorist desenvolvido por Allen Newell, JC Shaw e Herbert Simon em 1956. Uma das coisas que um lógico faz é pegar um conjunto de declarações em lógica e deduzir as conclusões (declarações adicionais) que devem ser verdadeiras pelas leis da lógica. Por exemplo, se dado um sistema lógico que afirma "Todos os humanos são mortais" e "Sócrates é humano", uma conclusão válida é "Sócrates é mortal". Claro que este é um exemplo trivial . Em sistemas lógicos reais, as declarações podem ser numerosas e complexas. Percebeu-se desde cedo que esse tipo de análise poderia ser significativamente auxiliado pelo uso de computadores. O Logic Theorist validou o trabalho teórico de Bertrand Russell e Alfred North Whitehead em seu influente trabalho sobre lógica matemática chamado Principia Mathematica . Além disso, sistemas subsequentes foram utilizados por lógicos para validar e descobrir novos teoremas e provas lógicas.

## Aplicações lógicas para computadores

Sempre houve uma forte influência da lógica matemática no campo da inteligência artificial (IA). Desde o início do campo percebeu-se que a tecnologia para automatizar inferências lógicas poderia ter um grande potencial para resolver problemas e tirar conclusões a partir de fatos. Ron Brachman descreveu a lógica de primeira ordem (FOL) como a métrica pela qual todos os formalismos de representação de conhecimento de IA devem ser avaliados. Não há método conhecido mais geral ou poderoso para descrever e analisar informações do que o FOL. A razão pela qual o próprio FOL simplesmente não é usado como linguagem de computador é que ele é realmente muito expressivo, no sentido de que o FOL pode facilmente expressar declarações que nenhum computador, não importa o quão poderoso, poderia resolver . Por essa razão, toda forma de representação do conhecimento é, em certo sentido, uma troca entre expressividade e computabilidade. Quanto mais expressiva for a linguagem, quanto mais próxima estiver de FOL, mais provável será que ela seja mais lenta e propensa a um loop infinito.
Por exemplo, as regras SE ENTÃO usadas em sistemas especialistas se aproximam de um subconjunto muito limitado de FOL. Em vez de fórmulas arbitrárias com toda a gama de operadores lógicos, o ponto de partida é simplesmente o que os lógicos chamam de modus ponens . Como resultado, os sistemas baseados em regras podem suportar computação de alto desempenho, especialmente se tirarem vantagem de algoritmos de otimização e compilação.
Outra área importante de pesquisa para a teoria lógica foi a engenharia de software. Projetos de pesquisa como os programas Knowledge Based Software Assistant e Programmer's Apprentice aplicaram a teoria lógica para validar a exatidão das especificações de software. Eles também os usaram para transformar as especificações em código eficiente em diversas plataformas e provar a equivalência entre a implementação e a especificação. Essa abordagem orientada à transformação formal costuma ser muito mais trabalhosa do que o desenvolvimento de software tradicional . No entanto, em domínios específicos com formalismos apropriados e templates reutilizáveis, a abordagem ta se mostrado viável para produtos comerciais. Os domínios apropriados são geralmente aqueles como sistemas de armas, sistemas de segurança e sistemas financeiros em tempo real, onde a falha do sistema tem um custo humano ou financeiro excessivamente alto. Um exemplo de tal domínio é o projeto VLSI (Very Large Scale Integrated) — o processo para projetar os chips usados para as CPUs e outros componentes críticos de dispositivos digitais. Um erro em um chip é catastrófico. Ao contrário do software, os chips não podem ser corrigidos ou atualizados. Como resultado, há justificativa comercial para o uso de métodos formais para provar que a implementação corresponde à especificação.
Outra aplicação importante da lógica para a tecnologia de computadores tem sido na área de linguagens de quadros e classificadores automáticos. Linguagens de quadros como KL-ONE têm uma semântica rígida. As definições em KL-ONE podem ser mapeadas diretamente para a teoria dos conjuntos e o cálculo de predicados. Isso permite que provadores de teoremas especializados chamados classificadores analisem as várias declarações entre conjuntos, subconjuntos e relações em um determinado modelo. Desta forma, o modelo pode ser validado e quaisquer definições inconsistentes sinalizadas. O classificador também pode inferir novas informações, por exemplo, definir novos conjuntos com base em informações existentes e alterar a definição de conjuntos existentes com base em novos dados. O nível de flexibilidade é ideal para lidar com o mundo em constante mudança da Internet. A tecnologia do classificador é construída sobre linguagens como a Web Ontology Language para permitir um nível semântico lógico na Internet existente. Essa camada é chamada de web semântica.
A lógica temporal é usada para raciocinar em sistemas concorrentes .

## Veja também

* Lógica computacional
* Programação lógica