Lógica em ciência da computação

Lógica em ciência da computação abrange a sobreposição entre o campo da Lógica e o da ciência da computação. O tópico pode ser essencialmente dividido em três áreas principais:

• Fundamentos e análises teóricas.
• Uso da tecnologia da computação para auxiliar na lógica.
• O uso de conceitos da lógica para aplicações computacionais.

Representação diagramática de portas lógicas de computador

Fundamentos e análises teóricas

Os fundamentos mais essenciais para a ciência da computação são baseados em lógica e teoria dos conjuntos. O lógico Gottlob Frege, que definiu o primeiro cálculo proposicional, essencialmente criou a primeira linguagem de programação. A linguagem que ele definiu tem todos os requisitos formais para uma poderosa linguagem de programação e especificação de computadores. A teoria da computação baseia-se em conceitos definidos por lógicos e matemáticos, como Alonzo Church e Alan Turing. Além disso, algumas outras grandes áreas de sobreposição teórica entre a lógica e a ciência da computação são:

• O teorema da incompletude de Godel, que prova que qualquer sistema lógico conterá declarações que não são nem verdadeiras nem falsas. Isso tem aplicação direta em questões teóricas relativas à viabilidade de provar a completude e correção de software.
• O "problema do frame" é um problema básico que deve ser superado quando se usa a lógica para representar os objetivos e estado de um agente de inteligência artificial.
• A teoria das categorias é a análise formal e transformação dos grafos direcionados, uma área com inúmeras aplicações em ciência da computação. Por exemplo, os modelos orientados a objetos podem ser representados como categorias; e a tecnologia de prova de teoremas pode transformar as especificações do objeto modelo em código.
• O isomorfismo de Curry–Howard é uma prova sobre a relação entre sistemas lógicos e softwares. Esta teoria estabeleceu a base teórica para a visualização de um programa de computador como um enunciado da lógica formal que pode ser provado correto e consistente.

Computadores para ajudar lógicos

Uma das primeiras aplicações a usar o termo Inteligência Artificial foi o sistema Logic Theorist, desenvolvido por Allen Newell, J. C. Shaw e Herbert Simon, em 1956. Uma das coisas que um lógico faz é tomar um conjunto de instruções em Lógica e deduzir as conclusões (declarações adicionais) que devem ser verdadeiras pelas leis da lógica. Por exemplo, se for dado um sistema lógico que afirma "Todos os seres humanos são mortais" e "Sócrates é humano", uma conclusão válida é "Sócrates é mortal". É claro que isto é um exemplo trivial. Em sistemas lógicos reais, as declarações podem ser numerosas e complexas. Percebeu-se logo no início que este tipo de análise pode ser significativamente auxiliada pelo uso de computadores. Logic Theorist validou o trabalho teórico de Bertrand Russell e Alfred North Whitehead em seus trabalhos influentes na lógica matemática, chamado Principia Mathematica. Além disso, sistemas subsequentes têm sido utilizados pelos lógicos para validar e descobrir novos teoremas lógicos e provas.

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 as origens do campo, percebeu-se que a tecnologia para automatizar inferências lógicas pode ter um grande potencial para resolver problemas e tirar conclusões a partir de fatos. Ron Brachman descreveu a Lógica de Primeira Ordem (LPO) como métrica pela qual toda formalidade de representação do conhecimento de IA deve ser avaliada. Não existe um método mais geral ou poderoso conhecido para descrever e analisar informações como a LPO. A razão pela qual a própria LPO não é simplesmente utilizada como uma linguagem de computador é que ela é muito expressiva, no sentido de que pode facilmente expressar afirmações que nenhum computador, não importa quão poderoso, possa resolver. Por esta razão, todas as formas de representação do conhecimento são, em certo sentido, uma troca entre expressividade e computabilidade. Quanto mais expressiva for a linguagem, mais próxima da LPO, mais provável de ser lenta e propensa a um loop infinito ela será.

Por exemplo, regras do SE ENTÃO usadas no Sistema Especialista são um subconjunto muito limitado da LPO. Ao invés 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, a computabilidade de sistemas baseadas em regras pode ser muito boa, especialmente se elas se aproveitam de algoritmos de otimização e compilação.

Outra importante área de pesquisa para a teoria lógica foi a engenharia de software. Projetos de pesquisa, tais como os programas Knowledge Based Software Assistant e Programmer's Apprentice aplicaram a teoria lógica para validar a corretude de especificações de software. Esses programas também foram usados para transformar as especificações em código eficiente em diversas plataformas; e para provar a equivalência entre a implementação e a especificação. Esta abordagem é muitas vezes mais trabalhosa do que o desenvolvimento tradicional de software. No entanto, em domínios específicos com formalismos apropriados e modelos reutilizáveis, a abordagem mostrou-se viável para produtos comerciais. Os domínios apropriados são geralmente aqueles como os sistemas de armas, sistemas de segurança e sistemas financeiros em tempo real onde a falha do sistema tem custo financeiro ou humano excessivamente alto. Um exemplo de tal domínio é o design integrado de larga escala - o processo para criar os chips utilizados para CPUs e outros componentes críticos de dispositivos digitais. Um erro em um chip é catastrófico. Ao contrário de chips de software, não podem ser consertadas ou atualizadas. 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 à tecnologia computacional tem sido na área de linguagens frame e classificadores automáticos. Linguagens frame como KL-ONE tem semânticas rígidas. Definições em KL-ONE podem ser mapeadas diretamente à teoria dos conjuntos e o cálculo de predicados. Isso permite que especialistas em provar teoremas, chamados classificadores, analisem as diversas 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 sempre em mudança da Internet. Tecnologia classificadora é construída sobre linguagens como a OWL para permitir um nível semântico lógico para a Internet existente. Essa camada é a chamada web semântica.

Livros

• Ben-Ari, Mordechai (2003). 2nd ed. [S.l.]: Springer-Verlag. ISBN 1-85233-319-7 
• Huth, Michael; Ryan, Mark (2004). 2nd ed. [S.l.]: Cambridge University Press. ISBN 0-521-54310-X http://www.cs.bham.ac.uk/research/lics/ 
• Burris, Stanley N. (1997). [S.l.]: Prentice Hall. ISBN 0-13-285974-2 

Ligações externas

• Article on Logic and Artificial Intelligence at the Stanford Encyclopedia of Philosophy.
• IEEE Symposium on Logic in Computer Science (LICS)
• Alwen Tiu, Introduction to logic video recording of a lecture at ANU Logic Summer School '09 (aimed mostly at computer scientists)