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

Origem: Wikipédia, a enciclopédia livre.
Ir para: navegação, pesquisa
Broom icon.svg
As referências deste artigo necessitam de formatação (desde dezembro de 2016). Por favor, utilize fontes apropriadas contendo referência ao título, autor, data e fonte de publicação do trabalho para que o artigo permaneça verificável no futuro.
Representação esquemática de portas lógicas de um computador

A lógica em ciência da computação cobre os campos da lógica e da ciência da computação. O tópico pode essencialmente ser dividido em três áreas principais:

  • Fundamentos teóricos e análises;
  • Uso da tecnologia de computador para auxiliar a resolver problemas lógicos;
  • Utilização de conceitos de lógica para aplicações na computação.

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

A lógica desempenha um papel fundamental na ciência da computação. Algumas das principais áreas de lógica, que são particularmente significativos são a teoria da computabilidade (anteriormente chamada de teoria da recursão), lógica modal e teoria da categoria. A teoria da computação é baseada em conceitos definidos por lógicos e matemáticos como Alonzo Church e Alan Turing.[1][2] Church pela primeira vez mostrou a existência de problemas que não foram resolvidos através de algoritmos usando a sua noção de lambda-definição. Turing forneceu a primeira análise convincente do que pode ser chamado de procedimento mecânico e Kurt Gödel afirmou que ele achou a análise de  Turing"perfeita".[3] Além disso, algumas outras áreas que compõem os campos entre a lógica e ciência da computação são:

  • Teorema da incompletude de Gödel prova que qualquer sistema lógico poderoso o suficiente para caracterizar aritmética irá conter afirmações que não pode ser provado como verdadeiro nem falso dentro desse sistema. Isso tem aplicação direta para as questões teóricas relativas à viabilidade de provar a integridade e correção de um determinado software.[4]
  • O Problema de quadro (Frame problem) é um problema que deve ser superado quando usando lógica de primeira ordem para representar os objetivos e o estado de uma inteligência artificial agente.[5]
  • A correspondência de Curry-Howard (Curry-Howard correspondence) é uma relação entre sistemas lógicos e de softwares. Esta teoria estabelece uma correspondência precisa entre provas e programas. Em particular, mostrou que, os termos no de lambda-cálculo de tipo simples correspondem a provas da lógica proposicional intuicionista.
  • Categoria teoria representa uma visão da matemática que enfatiza as relações entre as estruturas. Ele está intimamente ligada a muitos aspectos da ciência da computação: sistemas de tipo de linguagens de programação, teoria da transição de sistemas, modelos de linguagens de programação e a teoria da linguagem de programação semântica.[6]

Computadores para auxiliar lógicos[editar | editar código-fonte]

Um dos primeiros aplicativos que usou o termo Inteligência Artificial foi o Logic Theorist sistema desenvolvido por Allen Newell, J. C. Shaw, e Herbert Simon , em 1956. Uma das coisas que um Lógico faz é tomar como base um conjunto de proposições em lógica e deduzir as conclusões (instruções adicionais) que devem ser verdadeiras, pelas leis da lógica. Por exemplo, Se dado um sistema lógico que afirma que "Todo homem é mortal" e "Sócrates é humano" uma conclusão válida é "Sócrates é mortal". É claro que isso é um exemplo trivial. Na lógica atual, as proposições podem ser complexas e numerosas. Percebeu-se então desde o início que esse tipo de análise poderia ser significativamente auxiliada pelo uso de computadores. O teórico da lógica validou o trabalho teórico de Bertrand Russell e Alfred North Whitehead , na sua influente obra de lógica matemática chamada Principia Mathematica. Além disso subsequentes sistemas têm sido utilizados pelos lógicos para validar e descobrir novos teoremas lógicos e provas.[7]

Lógica aplicada aos computadores[editar | editar código-fonte]

Sempre houve uma forte influência da lógica matemática no campo da Inteligência Artificial (AI). Desde o início do campo, percebeu-se que a tecnologia para automatizar deduções lógicas podiam ter grande potencial para resolver problemas e tirar conclusões a partir de fatos. Ron Brachman descreveu Lógica de Primeira Ordem (FOL) como uma métrica para que todo o formalismo de representação do conhecimento de IA deve ser avaliado. Não existe nenhum método mais geral ou poderoso conhecido para descrever e analisar informações do que FOL. A razão pelo que FOL não é simplesmente usada como uma linguagem de computador é que ele é realmente muito expressiva, no sentido em que FOL pode expressar facilmente declarações de que nenhum computador, não importa o quão poderoso seja poderia resolver. Por isso, toda a forma de representação de conhecimento é, em algum sentido, um trade-off entre expressividade e computabilidade. Quanto mais expressiva é a linguagem, quanto mais próxima for de FOL, mais propenso à ser lento e a executar loop infinito.[8]

Por exemplo, as regras IF THEN, usadas em Sistemas Especialistas são um subconjunto muito limitado da 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, a computabilidade dos sistemas baseados em regras podem ser pode ser muito bom, especialmente se eles aproveitam-se de algoritmos de otimização e de compilação.[9]

Outra área importante de pesquisa para a lógica teórica foi a engenharia de software. Projetos de pesquisa, tais como o Knowledge-Based Software Assistant, e os aprendizes de programador aplicam a lógica teórica para validar a exatidão das especificações do software. Eles também usaram para transformar as especificações em um código eficiente em diversas plataformas e para provar a equivalência entre a implementação e a especificação.[10] Esta abordagem formal de transformação muitas vezes é muito mais esforço do que o desenvolvimento do software tradicional. No entanto, em domínios específicos com formalismos adequados e modelos reutilizáveis, a abordagem tem se mostrado viável para produtos comerciais. Os domínios apropriados, normalmente, são aqueles que, como os sistemas de armas, sistemas de segurança, e em tempo real, onde a falha do sistema tem um custo humano ou financeiro excessivamente elevado. Um exemplo deste tipo de domínio é o projeto Very Large Scale Integrated (VLSI)—o projeto processa o design de chips utilizados por CPU's e outros componentes críticos de dispositivos digitais. Um erro em um chip, é catastrófico. Ao contrário dos softwares 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.[11]

Outra aplicação importante da lógica para a computação 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 diretamente mapeadas para a teoria dos conjuntos e o cálculo de predicados. Isso permite provedores de teoremas especializados chamados classificadores para analisar 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 Classifier é construída no topo das linguagens como o Web Ontology Language para permitir um nível semântico lógico existente para a Internet. Esta camada de é chamada de web semântica(Semantic web).

Lógica Temporal é usada para raciocínio, em sistemas concorrentes.[12]

Veja também[editar | editar código-fonte]

Referências

  1. [S.l.: s.n.] ISBN 0-13-273417-6  Em falta ou vazio |título= (ajuda)Falta o |titulo= (Ajuda)
  2. Rolf Herken (ed.). [S.l.: s.n.] https://books.google.com/books?id=YafIDVd1Z68C&pg=PA290#v=onepage&q&f=false  Em falta ou vazio |título= (ajuda)Falta o |titulo= (Ajuda)
  3. [S.l.: s.n.] https://books.google.ca/books?id=ulw3BAAAQBAJ&pg=PA118&lpg=PA118&dq=Godel+convinced+by+Turing's+analysis&source=bl&ots=Wa1PunvmLM&sig=yuj5GsarLT3PoTESY46s8L9x9rY&hl=en&sa=X&ved=0CCMQ6AEwAmoVChMIya2n8dGwxwIVUQmSCh0c8AIb#v=onepage&q=Godel%20convinced%20by%20Turing's%20analysis&f=false  Em falta ou vazio |título= (ajuda)Falta o |titulo= (Ajuda)
  4. [S.l.: s.n.] ISBN 978-0465026562  Em falta ou vazio |título= (ajuda)Falta o |titulo= (Ajuda)
  5. Citação vazia (ajuda) 
  6. [S.l.: s.n.]  Em falta ou vazio |título= (ajuda)Falta o |titulo= (Ajuda)
  7. Ed Feigenbaum (ed.). [S.l.: s.n.] ISBN 978-0262560924  Em falta ou vazio |título= (ajuda)Falta o |titulo= (Ajuda)
  8. Ronald Brachman and Hector J. Levesque (ed.). [S.l.: s.n.] ISBN 0-934613-01-X  Em falta ou vazio |título= (ajuda)Falta o |titulo= (Ajuda)
  9. 19. doi:10.1016/0004-3702(82)90020-0 
  10. (PDF) ftp://publications.ai.mit.edu/ai-publications/pdf/AIM-1004.pdf  Em falta ou vazio |título= (ajuda)
  11. [S.l.: s.n.] ISBN 0-521-443369 https://books.google.com/books?id=Hf_AZfW2YWsC&pg=PA14&lpg=PA14&dq=VLSI+chip+design+formal+methods&source=bl&ots=KzTJ7IrWmm&sig=jUvF19wOzfMqUGh4YQl5XzZrEfY&hl=en&sa=X&ei=W1K8Uu7YItXloASPsoCwCw&ved=0CDkQ6AEwAQ#v=onepage&q=VLSI%20chip%20design%20formal%20methods&f=false  Em falta ou vazio |título= (ajuda)Falta o |titulo= (Ajuda)
  12. Citação vazia (ajuda) 

Ler mais[editar | editar código-fonte]

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