Razão para aprender lógica proposicional e predicada

Compreendo a importância de que cientistas da computação ou qualquer engenheiro relacionado ao desenvolvimento de software tenham entendido o estudo da lógica básica como base.

Mas existem tarefas / trabalhos que exigem explicitamente o conhecimento sobre eles, além das tarefas que exigem qualquer tipo de representação de conhecimento usando Knowledge Base? Quero ouvir os tipos de tarefas, em vez de respostas conceituais.

A razão pela qual pergunto isso é apenas por minha curiosidade. Enquanto os estudantes de CS precisam dedicar um certo período de tempo a esse assunto, alguns cursos intensivos em praticidade (por exemplo, AI-Class ) ignoraram completamente esse tópico. E eu me pergunto que, por exemplo, o conhecimento predicate logicpode ajudar a desenhar, ER diagrammas pode não ser um requisito.

Atualização 27/5/2012) Obrigado por respostas. Agora eu acho que entendo e concordo totalmente com a importância do logicCS com sua grande quantidade de aplicações. Eu apenas escolhi a melhor resposta verdadeiramente pela impressionante impressão que obtive da solução para Windowso problema de tela azul.

Costumo gostar da Unificação e qualquer coisa relacionada a ela. Se você não conhece a lógica proposicional e predicada, está ignorando o básico da lógica. Se você tem interesse em qualquer coisa listada , seria como ter interesse em matemática e pular adição e multiplicação. A lógica não é apenas para IA.

Como resposta prática, lembre-se do problema do ponto flutuante da Intel e como você nunca mais os vê? Graças ao uso de provadores de teoremas, eles são coisa do passado. Lembre-se da tela azul da morte da Microsoft . Graças aos solucionadores SAT, verificação de modelo e outras soluções baseadas em lógica, eles são uma espécie em extinção.

Existem conexões extremamente profundas e difundidas entre lógica e ciência da computação. Para entender o que eles podem ser, lembre-se de que a ciência da computação também é chamada de "tecnologia da informação" ou "informática", o que significa que os sistemas de computador capturam, processam e entregam informações. Bem, a lógica é uma coisa semelhante. Ele estuda como as informações são capturadas em sentenças e como é possível que uma declaração seja uma conseqüência de outra, ou seja, como o conteúdo da informação já está presente em outra declaração (ou coleção de declarações). Nesse sentido, lógica e ciência da computação são essencialmente as mesmasdisciplina, com foco em diferentes aspectos. Os lógicos (Church, Kleene, Turing, Post e seus alunos e colegas) criaram a disciplina de Ciência da Computação, e muitos lógicos continuam a dar contribuições à Ciência da Computação, principalmente Jean-Yves Girard e seus alunos.

Aqui estão algumas aplicações padrão da lógica em Ciência da Computação:

• O design de circuitos digitais é inteiramente baseado na lógica da proposta, tanto que seus engenheiros o chamam de "design lógico" em vez de "design de circuito". Mesmo a escrita de um programa de computador costuma envolver a criação de sua "lógica". (Observe que "lógica", no último sentido, é uma ideia informal e não lógica formal, usada para se referir ao fluxo de informações através do programa e se está sendo processado corretamente.)

• A lógica predicada e seu primo matemático, a teoria dos conjuntos, são usados ​​em uma variedade de linguagens de computação , por exemplo, a linguagem SQL para consultas de bancos de dados relacionais. Existem também linguagens de programação baseadas na lógica, chamadas "linguagens de programação lógica".

• A representação do conhecimento , que você já mencionou, possui muitos formalismos baseados na lógica. Mesmo que use formalismos não lógicos, muitos deles ainda têm um significado lógico e, portanto, são baseados na lógica.

• A lógica probabilística, em que as declarações não têm apenas valores verdadeiros / falsos, mas níveis de certeza / incerteza, é cada vez mais a base para sistemas de aprendizado de máquina .

• Se você deseja declarar formalmente o que um programa faz, ou seja, fornecendo uma especificação de programa , você acabará usando alguma forma de linguagem lógica. De fato, existem muitas linguagens de especificação de programa, como Z e B, baseadas em lógica de predicados e teoria de conjuntos. Também existem linguagens de especificação baseadas em lógica equacional, como Larch. Os cientistas da computação geralmente inventam novas lógicas para representar as necessidades da ciência da computação, por exemplo, Hoare Logic e Separation Logic, ou desenvolvem várias formas subutilizadas de lógicas tradicionais, como lógica temporal e lógica modal, e as desenvolvem ainda mais.

• Se você deseja verificar se um programa faz o que deveria fazer, acaba usando não apenas a linguagem da lógica, mas todo o mecanismo da lógica: teoria da prova, teoria do modelo e procedimentos de decisão. A tecnologia de verificação agora está crescendo aos trancos e barrancos e espero que, em mais uma década, eles sejam usados ​​rotineiramente para quase todo o desenvolvimento de software.

De fato, as conexões entre lógica e ciência da computação são tão profundas e difundidas que eu diria que é difícil ser um bom cientista da computação sem uma compreensão completa da lógica.

A razão pela qual alguns cientistas da IA ​​subestimam a lógica no momento é que alguns dos primeiros desenvolvedores da IA ​​propuseram a lógica pronta para uso como uma ferramentaao invés de uma fundação. A IA, por sua própria natureza, promete entregar mágica. Não precisamos fazer o trabalho duro dos sistemas de programação para obter resultados. Eles seriam capazes de descobrir por si mesmos como produzir soluções porque seriam "inteligentes". A lógica parecia apontar o caminho, porque se os sistemas de computador entendessem a lógica e soubessem processar informações usando as regras da lógica, eles seriam capazes de fornecer mágica. Esse tipo de fé na lógica foi, em retrospecto, perdido. Em primeiro lugar, a lógica de prateleira é muito forte e muito fraca ao mesmo tempo. É forte demais no sentido de que as regras da lógica são gerais demais para conceber procedimentos eficazes. Também é muito fraco, porque é a lógica idealizada pelos matemáticos para as necessidades da matemática e não ter o vocabulário necessário para lidar com muitos outros tipos de informações do mundo real com as quais os sistemas de IA devem lidar (como incerteza, informações contextuais como tempo, mudança, conhecimento, agência e assim por diante). Portanto, a IA está passando por uma reação contrária à lógica. Mas acho que, quando eles superarem essa reação, os cientistas da IA ​​perceberão que todos os métodos mais recentes ainda são baseados emlógica, amplamente interpretada .

A lógica é fundamental para toda a ciência da computação teórica. Sem aprender isso, você não será capaz de entender adequadamente a semântica da linguagem de programação, as máquinas de Turing, a programação lógica, a computabilidade e assim por diante. Mesmo o raciocínio sobre seus programas será mais difícil sem ele. Certamente, tentar fazer uma prova matemática de algum conceito de CS é praticamente impossível.

Ou talvez você esteja perguntando sobre usos na indústria. A lógica da aprendizagem forma a base para aprender a raciocinar com clareza e ver brechas nos argumentos de outras pessoas. A lógica é fundamental, se você usa os símbolos formais ou não.

Uma das tarefas repetidas que praticantes e teóricos da SC enfrentam é ganhar confiança na correção de seu código.

Existem duas abordagens principais:

1. Prova: crie uma prova lógica de que parte de um sistema possui certas propriedades, possivelmente auxiliadas por pré-condições, projeto por contrato e verificadores de código.
2. Teste: teste se determinadas propriedades são válidas para uma variedade de entradas e, em seguida, induza que essa propriedade é válida para outras entradas.

A primeira, baseada em métodos lógicos, geralmente é a única opção quando

1. Não há entrada típica. Por exemplo, ao testar propriedades de segurança, são as entradas atípicas com as quais você deve se preocupar, a menos que consiga raciocinar logicamente sobre quais entradas são atípicas, é improvável que você obtenha uma boa cobertura.
2. O espaço de configuração é muito grande, portanto, você deve decompô-lo em partes, racionalizando logicamente sobre quais partes podem afetar quais outras partes antes de testar localmente.
3. Você tem apenas documentação descrevendo o comportamento de caso de extremidade de sistemas fora de seu controle. Você pode simulá-los, mas não pode testar o que acontece quando uma dependência externa falha porque você não é capaz de causar falhas por razões legais ou éticas.

O teste empírico na ausência de uma prova é basicamente um substituto para a prova. Ao projetar um sistema para ser testável, você está criando um esboço de prova em que preenche partes da prova com "teste X, Y e Z aqui". A capacidade de raciocinar logicamente é essencial para poder arquitetar um sistema testável. Se o sistema não puder ser testado ou provado, seu designer / arquiteto não tem como negar que é adequado para o uso pretendido.

Dois campos mais importantes em que a lógica desempenha papel vital são:

1. Especificação e verificação formal de linguagem .
2. Classes tratáveis ​​de parâmetros fixos .

$Z$

Em resumo: 1. A definição de linguagem precisa de lógica, 2: A justiça de seus procedimentos precisa de lógica, 3. os procedimentos de verificação precisam de lógica.

Devo mencionar que isso é diferente do design do compilador ou ..., Esta é a definição "formal" de linguagens, a principal razão para fazer isso é provar a exatidão da linguagem ou modelo, tendo também uma prova formal. Isso pode ser usado na verificação de modelos de software, localizando erros antes da implementação, localizando impasses novamente antes da implementação, ...., Para o software que simula isso, você pode dar uma olhada no NModel .

Agora, por que, nos problemas tratáveis ​​de parâmetros fixos, você precisa trabalhar com a lógica? Você pode dividir as classes de rastreabilidade dos parâmetros fixos com diferentes níveis de lógica, elas podem ser convertidas entre si: lógica para automatizar, automação para representar graficamente e vice-versa, mas se Como você é um especialista em lógica, pode dividir e decidir sobre eles simplesmente, o teorema mais importante (depois do teorema de Robertson e Seymour ), nesse campo é o teorema de Courcelle . para obter mais informações, leia a pesquisa do teorema meta-algorítmico .