Lógica

Visão geral

Lógica é uma família de linguagens formais (formal languages) e métodos de inferência (inference methods) usados para representar conhecimento com precisão e para derivar consequências a partir desse conhecimento. Na I.A. clássica/simbólica (classical/symbolic AI), a lógica fornece uma base para representação de conhecimento (knowledge representation): expressar fatos, regras e relacionamentos de um modo que sustente raciocínio correto e explicável.

Este artigo foca em:

  • Lógica proposicional (propositional logic): raciocínio com variáveis booleanas (Boolean variables) (afirmações verdadeiro/falso).
  • Lógica de primeira ordem (first-order logic, FOL): raciocínio com objetos, propriedades, relações e quantificação (“para todo”, “existe”).

A lógica dá sustentação a muitos sistemas de I.A.: sistemas especialistas baseados em regras, provadores automáticos de teoremas (automated theorem provers), ferramentas de verificação (verification tools), solucionadores de restrições (constraint solvers; SAT/SMT) e linguagens de ontologia (ontology languages). Ela também se conecta a abordagens modernas como I.A. Neuro-Simbólica e aprendizado fracamente supervisionado (weakly supervised learning) a partir de regras.

Para representações mais orientadas a grafos e ontologias, que frequentemente se baseiam em ideias lógicas, veja Regras, Ontologias, Grafos de Conhecimento.

Conceitos centrais: sintaxe vs. semântica

A lógica separa claramente:

  • Sintaxe (syntax): como as expressões são formadas (símbolos e gramática).
  • Semântica (semantics): o que as expressões significam (verdade em relação a um modelo/mundo).

Duas noções semânticas centrais:

  • Satisfatível (satisfiable): um conjunto de fórmulas é satisfatível se alguma atribuição/modelo as torna todas verdadeiras.
  • Consequência lógica (entailment): uma base de conhecimento (knowledge base, KB) acarreta (entails) uma afirmação se todo modelo da base de conhecimento torna a afirmação verdadeira.

Notação comumente usada:

  • ( \models ) (“acarreta” no sentido semântico): ( KB \models \varphi )
  • ( \vdash ) (“deriva/prova” em um sistema de prova): ( KB \vdash \varphi )

Um bom sistema de raciocínio busca:

  • Correção (soundness): se ( KB \vdash \varphi ), então ( KB \models \varphi ) (nunca prova consequências falsas).
  • Completude (completeness): se ( KB \models \varphi ), então ( KB \vdash \varphi ) (consegue provar todas as consequências verdadeiras, ao menos em princípio).

Lógica proposicional

Linguagem e operadores

A lógica proposicional usa átomos (atoms) (variáveis proposicionais) como (P, Q, R) que representam afirmações inteiras:

  • (P): “Está chovendo.”
  • (Q): “O chão está molhado.”

Fórmulas são construídas usando conectivos:

  • Negação: ( \lnot P )
  • Conjunção: ( P \land Q )
  • Disjunção: ( P \lor Q )
  • Implicação: ( P \rightarrow Q )
  • Bicondicional: ( P \leftrightarrow Q )

Uma atribuição de verdade (truth assignment) mapeia cada átomo para Verdadeiro/Falso, e a verdade de uma fórmula composta segue as tabelas-verdade (truth tables) usuais.

Exemplo: raciocinando com implicações

Suponha que modelamos:

  1. ( R \rightarrow W ) (“Se chover, o chão fica molhado”)
  2. ( R ) (“Está chovendo”)

Então podemos inferir (W) via modus ponens (modus ponens):

  • De (P \rightarrow Q) e (P), conclua (Q).

Em notação de prova:

  • ( {R \rightarrow W, R} \vdash W )

Formas normais e por que elas importam

Raciocínio automatizado frequentemente converte fórmulas para formatos padrão.

Forma Normal Conjuntiva (Conjunctive Normal Form, CNF) é uma conjunção de cláusulas, em que cada cláusula é uma disjunção de literais:

  • Literal: (P) ou (\lnot P)
  • Cláusula: ((P \lor \lnot Q \lor R))
  • CNF: ((P \lor Q) \land (\lnot P \lor R))

Muitos solucionadores de SAT (SAT solvers) exigem CNF.

Exemplo de conversão (esboço):

  • ( (A \rightarrow B) ) torna-se ( (\lnot A \lor B) )
  • ( (A \leftrightarrow B) ) torna-se ( (A \rightarrow B) \land (B \rightarrow A) )

Resolução (proposicional)

Resolução (resolution) é uma regra de inferência chave para CNF. Se você tem:

  • ( (P \lor Q) )
  • ( (\lnot P \lor R) )

Você pode resolver em (P) para derivar:

  • ( (Q \lor R) )

A resolução é fundamental em SAT e em prova de teoremas. Uma estratégia comum de prova é a refutação (refutation):

Para provar (KB \models \varphi), mostre que (KB \land \lnot \varphi) é insatisfatível (leva a uma contradição).

Complexidade e solucionadores práticos

  • SAT (satisfatibilidade (satisfiability) da lógica proposicional) é NP-completo (NP-complete).
  • Apesar da dificuldade no pior caso, solucionadores de SAT modernos conseguem lidar com milhões de variáveis em muitos problemas reais usando:
    • Aprendizado de cláusulas guiado por conflitos (conflict-driven clause learning, CDCL)
    • Propagação unitária (unit propagation) eficiente
    • Heurísticas para ramificação (branching) e reinícios (restarts)

SAT é amplamente usado em escalonamento, verificação, configuração e planejamento.

Exemplo prático: restrições como lógica proposicional

Imagine uma restrição pequena de escalonamento:

  • Exatamente um entre (A) ou (B) é selecionado: ( (A \lor B) \land \lnot(A \land B) )

Em forma CNF:

  • ( (A \lor B) \land (\lnot A \lor \lnot B) )

Adicione outra regra:

  • Se (A) então (C): (A \rightarrow C \equiv \lnot A \lor C)

Um solucionador de SAT pode então buscar atribuições para (A, B, C) que satisfaçam todas as restrições.

Lógica de primeira ordem (FOL)

A lógica proposicional trata afirmações como indivisíveis. A lógica de primeira ordem aumenta a expressividade ao falar sobre objetos e relações.

Blocos de construção

A FOL inclui:

  • Constantes (constants): objetos específicos (por exemplo, alice, bob)
  • Variáveis (variables): x, y
  • Predicados (predicates) (relações/propriedades): Parent(x, y), Human(x)
  • Funções (functions): mapeiam objetos em objetos, como MotherOf(x)
  • Quantificadores (quantifiers):
    • Universal: ( \forall x , \varphi(x) ) (“para todo x”)
    • Existencial: ( \exists x , \varphi(x) ) (“existe um x”)
  • Opcionalmente, igualdade (equality) (=)

Uma interpretação (interpretation) em FOL especifica:

  • Um domínio de objetos
  • A que cada constante se refere
  • Quais tuplas satisfazem cada predicado
  • Como funções mapeiam elementos do domínio

Exemplo: uma pequena base de conhecimento

Fatos:

  • Human(alice)
  • Human(bob)
  • Parent(alice, bob)

Regra:

  • “Todos os pais são humanos”: [ \forall x \forall y , (Parent(x,y) \rightarrow Human(x)) ]

Consulta:

  • A base de conhecimento acarreta Human(alice)? Sim (fato direto).
  • Ela acarreta Human(bob)? Sim (fato).
  • Ela acarreta Human(x) para todo x? Não; a base de conhecimento não descreve todo o domínio.

Quantificadores e escopo

Quantificadores importam muito:

  • ( \forall x \exists y , Loves(x,y) ): todo mundo ama alguém (possivelmente um y diferente para cada x)
  • ( \exists y \forall x , Loves(x,y) ): existe um y especial amado por todos

Estas são afirmações bem diferentes.

Inferência em FOL: unificação e substituição

Muitos procedimentos de prova em FOL dependem de unificação (unification): encontrar uma substituição que torne duas expressões idênticas.

Exemplo:

  • Parent(x, bob) e Parent(alice, y) unificam com a substituição {x := alice, y := bob}.

A unificação é uma ferramenta central por trás da programação lógica (por exemplo, encadeamento para trás no estilo Prolog) e da resolução em FOL.

Resolução em FOL (alto nível)

A resolução em FOL normalmente envolve:

  1. Eliminar implicações
  2. Empurrar negações para dentro
  3. Padronizar variáveis para evitar colisões
  4. Mover quantificadores para fora (forma prenexa (prenex form))
  5. Skolemizar (Skolemize) quantificadores existenciais (substituir variáveis existenciais por funções/constantes de Skolem)
  6. Remover quantificadores universais (implicitamente universais nas cláusulas)
  7. Converter para CNF e aplicar resolução + unificação

Ressalva importante: validade/consequência lógica em FOL completa é semi-decidível (semi-decidable):

  • Se uma afirmação é acarretada, um provador completo pode eventualmente encontrar uma prova.
  • Se ela não é acarretada, o provador pode rodar para sempre.

Fragmentos decidíveis e úteis

Como a FOL completa é muito expressiva, sistemas práticos frequentemente usam fragmentos com melhores propriedades computacionais:

  • Cláusulas de Horn (Horn clauses): cláusulas com no máximo um literal positivo
    Permitem encadeamento para frente/para trás eficiente; fundamento para raciocínio no estilo Datalog.
  • Datalog (lógica de Horn sem funções): frequentemente decidível e eficiente; amplamente usado em bancos de dados e análise estática.
  • Lógicas de descrição (description logics): fragmentos adaptados, usados em ontologias (por exemplo, OWL); veja também Lógicas de Descrição.

Tarefas de raciocínio em I.A.

A lógica sustenta várias tarefas padrão:

  • Consequência lógica / resposta a consultas (query answering): (KB \models \varphi)?
  • Verificação de consistência (consistency checking): (KB) é satisfatível?
  • Explicação (explanation): qual subconjunto da base de conhecimento sustenta uma conclusão (rastro de prova (proof trace))?
  • Abdução (abduction): encontrar hipóteses (H) tais que (KB \land H \models \varphi) (comum em diagnóstico)
  • Planejamento como inferência (planning as inference): codificar ações e restrições logicamente; buscar um modelo satisfatível (frequentemente via SAT)

Muitas dessas se conectam a Problemas de Satisfação de Restrições, Solucionadores de SAT e Solucionadores de SMT.

Aplicações práticas

1) Sistemas especialistas e raciocínio baseado em regras

Sistemas especialistas (expert systems) clássicos codificam conhecimento de domínio como regras lógicas:

  • Se Symptom(x, fever) e Symptom(x, rash) então PossibleDisease(x, measles).

Com mecanismos de regras apropriados, você pode executar:

  • Encadeamento para frente (forward chaining) (orientado a dados): deriva todas as consequências a partir dos fatos.
  • Encadeamento para trás (backward chaining) (orientado a objetivos): tenta provar uma consulta específica.

Essas abordagens são centrais em muitos sistemas de regras de negócio e diagnósticos.

2) Representação de conhecimento e ontologias

Ontologias frequentemente dependem de semântica baseada em lógica:

  • Relações de classe/subclasse
  • Restrições de propriedades
  • Inferência de fatos implícitos

Embora grafos de conhecimento (knowledge graphs) tenham estrutura em grafo, seu significado é frequentemente fundamentado em formalismos lógicos. Para uma visão mais ampla, veja Regras, Ontologias, Grafos de Conhecimento.

3) Verificação, segurança e análise de programas

A lógica é amplamente usada para provar propriedades de sistemas:

  • Checagem de equivalência de hardware (SAT)
  • Verificação de modelos de propriedades temporais (frequentemente reduz a SAT/SMT)
  • Prova de invariantes de programas (SMT, raciocínio no estilo lógica de Hoare)

Essas aplicações são importantes em I.A. crítica para segurança e em infraestrutura de software robusta.

4) Planejamento e satisfatibilidade

Muitos problemas de planejamento podem ser codificados como SAT:

  • Variáveis representam se uma ação ocorre no tempo (t)
  • Restrições impõem pré-condições e efeitos
  • Uma atribuição satisfatível corresponde a um plano válido

Isso faz a ponte entre lógica e Planejamento e busca clássica.

5) Aprendizado com lógica (e lógica com aprendizado)

A lógica também interage com o aprendizado de máquina (machine learning, ML):

  • Programação Lógica Indutiva (Inductive Logic Programming, ILP) aprende regras lógicas a partir de exemplos e conhecimento de fundo: Programação Lógica Indutiva.
  • Redes Lógicas de Markov (Markov Logic Networks, MLNs) combinam lógica de primeira ordem com pesos probabilísticos (probabilistic weights) para lidar com incerteza: Redes Lógicas de Markov.
  • Métodos neuro-simbólicos (neuro-symbolic methods) integram percepção neural com restrições lógicas ou raciocínio diferenciável (differentiable reasoning): I.A. Neuro-Simbólica.

A lógica contribui com estrutura, restrições e interpretabilidade (interpretability); o aprendizado de máquina contribui com robustez (robustness) a ruído e dados brutos (visão, texto, fala).

Escolhas comuns de modelagem e armadilhas

Mundo aberto vs. mundo fechado

A lógica clássica tipicamente segue uma hipótese do mundo aberto (open world assumption): se algo não é conhecido, é desconhecido, não falso.

Muitos sistemas de banco de dados/regras usam uma hipótese do mundo fechado (closed world assumption): o que não é conhecido é assumido falso. Isso é prático, mas muda a semântica.

Escolher entre essas alternativas afeta resultados de consultas e como você representa padrões (defaults).

Igualdade e nomes únicos

  • Constantes diferentes se referem a objetos diferentes? (Hipótese de Nomes Únicos (Unique Names Assumption))
  • Raciocinamos com axiomas explícitos de igualdade?

Em muitos cenários de representação de conhecimento, você precisa decidir como a identidade é tratada, especialmente ao integrar fontes de dados.

Expressividade vs. computabilidade

Linguagens mais expressivas podem modelar mais, mas podem se tornar mais difíceis (ou impossíveis) de decidir automaticamente:

  • Lógica proposicional: decidível, mas pode ser cara (NP-completa).
  • FOL completa: semi-decidível; pode não terminar.
  • Lógicas restritas (Horn/Datalog/lógicas de descrição): frequentemente decidíveis e eficientes para tarefas-chave.

Uma regra prática: use a lógica mais fraca que consiga expressar o que você precisa.

Mini-exemplo trabalhado: do inglês à lógica à inferência

Afirmações em inglês:

  1. “All humans are mortal.”
  2. “Socrates is a human.”
  3. Therefore, “Socrates is mortal.”

Codificação em FOL:

  1. ( \forall x , (Human(x) \rightarrow Mortal(x)) )
  2. ( Human(socrates) )
  3. Consulta: ( Mortal(socrates) )

Uma prova simples usa instanciação universal + modus ponens:

  • De (1), instancie (x := socrates): ( Human(socrates) \rightarrow Mortal(socrates) )
  • Com (2), conclua ( Mortal(socrates) )

Isso ilustra por que a FOL é uma escolha natural para representar regras gerais junto com fatos específicos.

Resumo

A lógica continua sendo uma ferramenta central na I.A. clássica/simbólica para representar conhecimento e realizar raciocínio formal:

  • Lógica proposicional é simples, decidível e alimenta aplicações baseadas em SAT.
  • Lógica de primeira ordem é muito mais expressiva, permitindo conhecimento baseado em objetos e relações, mas introduz problemas de raciocínio mais difíceis.
  • Sistemas práticos de I.A. frequentemente usam fragmentos restritos (cláusulas de Horn, Datalog, lógicas de descrição) e dependem de solucionadores poderosos (SAT/SMT) ou mecanismos de regras.
  • A lógica continua relevante na I.A. moderna por meio de verificação, planejamento, ontologias e extensões neuro-simbólicas e probabilísticas.

Ao construir sistemas baseados em conhecimento, a lógica fornece não apenas uma linguagem de representação, mas um modo disciplinado de conectar significado, inferência e explicação.