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

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

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[editar | editar código-fonte]

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 .[1][2] 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".[3] 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.[4]
  • 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.[5]
  • 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.[6]

Computadores para ajudar os 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 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.[7]

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

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

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

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

A lógica temporal é usada para raciocinar em sistemas concorrentes .[14]

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

Referências[editar | editar código-fonte]

  1. ↑ Lewis, Harry R. (1981). Elements of the Theory of Computation. [S.l.]: Prentice Hall 
  2. ↑ Davis, Martin (11 de maio de 1995). «Influences of Mathematical Logic on Computer Science». In: Rolf Herken. The Universal Turing Machine. [S.l.]: Springer Verlag. ISBN 9783211826379 
  3. ↑ Kennedy, Juliette (21 de agosto de 2014). Interpreting Godel. [S.l.]: Cambridge University Press. ISBN 9781107002661. Consultado em 17 de agosto de 2015 
  4. ↑ Hofstadter, Douglas R. (5 de fevereiro de 1999). Gödel, Escher, Bach: An Eternal Golden Braid. [S.l.]: Basic Books. ISBN 978-0465026562 
  5. ↑ McCarthy, John; P.J. Hayes (1969). «Some philosophical problems from the standpoint of artificial intelligence» (PDF). Machine Intelligence. 4: 463–502 
  6. ↑ Barr, Michael; Charles Wells (1998). Category Theory for Computing Science (PDF). [S.l.]: Centre de Recherches Mathématiques 
  7. ↑ Newell, Allen; J.C. Shaw; H.C. Simon (1963). «Empirical explorations with the logic theory machine». In: Ed Feigenbaum. Computers and Thought. [S.l.]: McGraw Hill. pp. 109–133. ISBN 978-0262560924 
  8. ↑ Levesque, Hector; Ronald Brachman (1985). «A Fundamental Tradeoff in Knowledge Representation and Reasoning». In: Ronald Brachman and Hector J. Levesque. Reading in Knowledge Representation. [S.l.]: Morgan Kaufmann. ISBN 0-934613-01-X. The good news in reducing KR service to theorem proving is that we now have a very clear, very specific notion of what the KR system should do; the bad new is that it is also clear that the services can not be provided... deciding whether or not a sentence in FOL is a theorem... is unsolvable. 
  9. ↑ Forgy, Charles (1982). «Rete: A Fast Algorithm for the Many Pattern/Many Object Pattern Match Problem*» (PDF). Artificial Intelligence. 19: 17–37. doi:10.1016/0004-3702(82)90020-0. Consultado em 25 de dezembro de 2013. Cópia arquivada (PDF) em 27 de dezembro de 2013 
  10. ↑ Rich, Charles; Richard C. Waters (novembro de 1987). «The Programmer's Apprentice Project: A Research Overview» (PDF). IEEE Expert. Consultado em 26 de dezembro de 2013. Cópia arquivada (PDF) em 6 de julho de 2017 
  11. ↑ Stavridou, Victoria (1993). Formal Methods in Circuit Design. [S.l.]: Press Syndicate of the University of Cambridge. ISBN 0-521-443369. Consultado em 26 de dezembro de 2013 
  12. ↑ MacGregor, Robert (junho de 1991). «Using a description classifier to enhance knowledge representation». IEEE Expert. 6 (3): 41–46. doi:10.1109/64.87683 
  13. ↑ Berners-Lee, Tim; James Hendler; Ora Lassila (17 de maio de 2001). «The Semantic Web A new form of Web content that is meaningful to computers will unleash a revolution of new possibilities». Scientific American. 284: 34–43. doi:10.1038/scientificamerican0501-34. Cópia arquivada em 24 de abril de 2013 
  14. ↑ Colin Stirling (1992). D. M. Gabbay; T. S. E. Maibaum, eds. Modal and Temporal Logics. II. Oxford University Press. pp. 477–563. ISBN 0-19-853761-1 

Leitura adicional[editar | editar código-fonte]

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

Obtida de "https://pt.wikipedia.org/w/index.php?title=Lógica_na_ciência_da_computação&oldid=67194837"