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

Origem: Wikipédia, a enciclopédia livre.
Ir para: navegação, pesquisa
Ambox important.svg
Foram assinalados vários aspectos a serem melhorados nesta página ou secção:
Diagrammatic Representation of Computer Logic Gates

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

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

Fundamentos e análises teóricas[editar | editar código-fonte]

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 se baseia em conceitos definidos pelos lógicos e matemáticos, como Alonzo Church e Alan Turing.[1] [2] 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 prova que qualquer sistema lógico conterá declarações que são nem verdadeiros nem falsos. Isso tem aplicação direta em questões teóricas relativas à viabilidade de provar a completude e corretude de software.[3]
  • O "problema do frame" é um problema básico que deve ser superado quando usa-se a lógica para representar os objetivos e estado de um agente de inteligência artificial.[4]
  • 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 tecnologia de prova de teoremas pode transformar as especificações do objeto-modelo em código.[5]
  • O isomorfismo de Curry–Howard é uma prova sobre a relação entre sistemas lógicos e software. 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[editar | editar código-fonte]

Uma das primeiras aplicações a usar o termo Inteligência Artificial foi o sistema Logic Theorist desenvolvido por Allan Newll, JC Shaw, e Herb 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 Russel e Alfred North Whitehead em seus trabalhos influentes na lógica matemática chamado Principia Mathematica. Além disso sistemas subseqüentes têm sido utilizados pelos lógicos para validar e descobrir novos teoremas lógicos e provas.[6]

Aplicações lógicas para computadores[editar | editar código-fonte]

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 conhecemento 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 é na verdade muito expressiva, no sentido de que a LPO 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 é, em certo sentido, uma troca entre expressividade e computabilidade. Quanto mais expressiva for a linguagem, mais próxima da LPO, mais provável ser lenta e propensa a um loop infinito.[7]

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.[8]

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.[9] Esta abordagem é muitas vezes mais trabalhoso 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.[10]

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.[11] [12]

Referências

  1. Lewis, Harry R.; Christos H. Papadimitriou. Elements of the Theory of Computation. Englewood Cliffs, New Jersey: Prentice-Hall, 1981. ISBN 0-13-273417-6.
  2. Davis, Martin. In: Rolf Herken. The Universal Turing Machine. [S.l.]: Springer Verlag. Visitado em 26 December 2013.
  3. Hofstadter, Douglas R.. Gödel, Escher, Bach: An Eternal Golden Braid. [S.l.]: Basic Books. ISBN 978-0465026562.
  4. McCarthy, J; P.J. Hayes. (1969). "Some philosophical problems from the standpoint of artificial intelligence". Machine Intelligence 4: 463-502.
  5. DeLoach, Scott; Thomas Hartrum. (June 2000). "A Theory Based Representation for Object-Oriented Domain Models". IEEE Transactions on Software Engineering 25 (6).
  6. Newell, Allen; J.C. Shaw and H.C. Simon. In: Ed Feigenbaum. Computers and Thought. [S.l.]: McGraw Hill, 1963. 109-133 pp. ISBN 978-0262560924.
  7. Levesque, Hector; Ronald Brachman. In: Ronald Brachman and Hector J. Levesque. Reading in Knowledge Representation. [S.l.]: Morgan Kaufmann, 1985. p. 49. ISBN 0-934613-01-X.
  8. Forgy, Charles. (1982). "Rete: A Fast Algorithm for the Many Pattern/Many Object Pattern Match Problem*". Artificial Intelligence 19: 17-37.
  9. Rich, Charles; Richard C. Waters. (November 1987). "The Programmer's Apprentice Project: A Research Overview". IEE Expert Special Issue on the Interactions between Expert Systems and Software Engineering.
  10. Stavridou, Victoria. Formal Methods in Circuit Design. [S.l.]: Press Syndicate of the University of Cambridge, 1993. ISBN 0-521-443369. Visitado em 26 December 2013.
  11. MacGregor, Robert. (June 1991). "Using a description classifier to enhance knowledge representation". IEEE Expert 6 (3).
  12. Berners-Lee, Tim; James Hendler and Ora Lassila. (May 17, 2001). "The Semantic Web A new form of Web content that is meaningful to computers will unleash a revolution of new possibilities". Scientific American.

Livros[editar | editar código-fonte]

Ligações externas[editar | editar código-fonte]