Representação do Conhecimento, Lógica e Inferência

Um algoritmo genético encontra uma boa configuração sem precisar explicar por que ela é boa. Um agente baseado em conhecimento enfrenta a exigência oposta: precisa representar afirmações sobre o mundo e derivar conclusões que sejam consequência delas. A diferença entre está na base e segue da base é o território da lógica.

A lógica separa duas camadas que a conversa cotidiana mistura. A sintaxe determina quais expressões são bem formadas e como podem ser manipuladas. A semântica determina em quais interpretações essas expressões são verdadeiras. Um mecanismo de inferência opera sobre símbolos, mas sua legitimidade depende de preservar significado. Sem essa ponte, teríamos apenas edição de texto com pretensões filosóficas.

1. Conhecimento e inferência

Uma base de conhecimento, abreviada como KB, de knowledge base, é um conjunto de sentenças em uma linguagem formal. A operação TELL acrescenta uma sentença; ASK pergunta se uma consulta decorre do que foi armazenado. Um agente baseado em conhecimento percebe o ambiente, traduz a percepção em sentenças, atualiza a KB, consulta o que fazer e registra a ação.

Conhecimento explícito tem uma vantagem de engenharia: podemos inspecionar premissas, regras e conclusões separadamente. A desvantagem é igualmente clara: alguém precisa escolher a linguagem, adquirir o conhecimento e manter a base consistente. A lógica não fabrica fatos e não corrige uma premissa falsa; ela mostra o que decorre das premissas dadas.

Chamaremos de modelo uma interpretação que atribui significado aos símbolos. Na lógica proposicional, um modelo é apenas uma atribuição de verdadeiro ou falso a cada proposição. Se há $n$ símbolos, existem $2^n$ modelos. Com três proposições, a semântica cabe em uma tabela de oito linhas; com cem, a enumeração ingênua exigiria $2^{100}$ linhas. A definição é simples, mas a escala cobra juros.

2. Lógica proposicional

Uma proposição atômica é um símbolo, como $p$, que pode ser verdadeiro ou falso. Sentenças compostas usam negação $\neg$, conjunção $\wedge$, disjunção $\vee$, implicação $\to$ e bicondicional $\leftrightarrow$. A implicação é falsa apenas quando o antecedente é verdadeiro e o consequente é falso:

Uma fórmula é satisfatível quando é verdadeira em pelo menos um modelo, válida quando é verdadeira em todos e insatisfatível quando não é verdadeira em nenhum. Essas classes não são três graus de qualidade. Uma fórmula válida não descreve um fato específico do mundo; ela expressa uma estrutura que vale sob qualquer atribuição.

Considere

Ela formaliza a transitividade da implicação. Em qualquer modelo no qual $p$ seja verdadeiro, as duas premissas forçam $q$ e depois $r$; se $p$ for falso, $p\to r$ já é verdadeiro. Logo $\varphi$ é válida. A tabela completa confirma oito linhas verdadeiras.

Exercícios resolvidos

1. Verifique se $\varphi$ acima é tautologia.

Solução:

Para $p$ falso, $p\to r$ é verdadeiro. Para $p$ verdadeiro, as premissas $p\to q$ e $q\to r$ forçam $q$ e $r$. Não existe linha falsa; a fórmula é válida.

2. A fórmula $p\wedge\neg p$ é satisfatível?

Solução:

Não. Nenhum modelo torna $p$ e sua negação verdadeiros ao mesmo tempo.

3. Prove $\neg(p\wedge q)\equiv\neg p\vee\neg q$.

Solução:

Para as quatro atribuições de $p$ e $q$, os dois lados têm a sequência $F,V,V,V$. As colunas idênticas estabelecem a equivalência.

4. Quantos modelos satisfazem $p\vee q\vee r$?

Solução:

Dos oito modelos, apenas $(F,F,F)$ torna a disjunção falsa. Há sete modelos.

5. Classifique $p\vee\neg p$, $p\wedge q$ e $p\wedge\neg p$.

Solução:

A primeira é válida; a segunda é satisfatível, mas não válida; a terceira é insatisfatível.

3. Consequência lógica

Escrevemos

quando todo modelo que satisfaz a base também satisfaz $\alpha$. Se $M(\varphi)$ é o conjunto de modelos de $\varphi$, então

Essa é uma relação semântica. Já $\mathrm{KB}\vdash_i\alpha$ afirma que o procedimento sintático $i$ deriva $\alpha$. Um procedimento é correto, ou sound, quando só deriva consequências verdadeiras:

É completo quando consegue derivar toda consequência:

Corretude impede conclusões inventadas; completude impede consequências verdadeiras eternamente fora de alcance. As duas propriedades são independentes. Um procedimento que nunca responde é correto por vacuidade e inútil por incompletude.

Há duas equivalências úteis:

e

A segunda transforma prova em refutação. Acrescentamos a negação da consulta e procuramos uma contradição.

4. Regras de inferência e resolução

O modus ponens diz que de $p$ e $p\to q$ podemos inferir $q$. A regra é correta porque não existe modelo em que as duas premissas sejam verdadeiras e $q$ seja falso.

A resolução trabalha com fórmulas em forma normal conjuntiva, ou FNC, uma conjunção de cláusulas, sendo cada cláusula uma disjunção de literais. Um literal é uma proposição ou sua negação. A regra proposicional é

Os literais complementares $\ell$ e $\neg\ell$ desaparecem. Para provar $\mathrm{KB}\models\alpha$, convertemos $\mathrm{KB}\wedge\neg\alpha$ para FNC e geramos resolventes. Derivar a cláusula vazia $\square$ significa que não há modelo, portanto a consulta é consequência da base.

Considere

Queremos provar $r$. Acrescentamos $\neg r$. Resolver $p\vee q$ com $\neg p$ produz $q$; resolver $q$ com $\neg q\vee r$ produz $r$; resolver $r$ com $\neg r$ produz $\square$.

Exercícios resolvidos

1. Converta $p\to(q\wedge r)$ para FNC.

Solução:

Eliminamos a implicação: $\neg p\vee(q\wedge r)$. Distribuindo, obtemos $(\neg p\vee q)\wedge(\neg p\vee r)$.

2. Prove que a KB acima implica $r$.

Solução:

Adicionamos $\neg r$ e derivamos $q$, depois $r$, depois $\square$. A refutação prova a consequência.

3. Aplique modus ponens a $p$, $p\to q$ e $q\to r$.

Solução:

De $p$ e $p\to q$, inferimos $q$; de $q$ e $q\to r$, inferimos $r$.

4. Resolva $p\vee q\vee s$ com $\neg q\vee r$.

Solução:

Eliminando $q$ e $\neg q$, o resolvente é $p\vee s\vee r$.

5. Mostre que ${p,\neg p}$ é insatisfatível.

Solução:

As duas cláusulas unitárias resolvem diretamente na cláusula vazia.

5. Lógica de primeira ordem

A lógica proposicional trata Ana é estudante como um bloco indivisível. A lógica de primeira ordem, ou FOL, de first-order logic, expõe objetos e relações. Podemos escrever

e

Os componentes básicos são constantes, variáveis, funções e predicados. Constantes nomeiam objetos; funções produzem termos; predicados afirmam relações; quantificadores universal $\forall$ e existencial $\exists$ dizem sobre quantos objetos falamos.

A semântica exige um domínio de objetos e uma interpretação para cada símbolo. A sentença universal não afirma que alguém seja estudante. Ela diz que, para qualquer objeto, ser estudante implica ser pessoa. Acrescentando $\operatorname{Estudante}(\operatorname{Ana})$, inferimos $\operatorname{Pessoa}(\operatorname{Ana})$.

O ganho expressivo tem custo. Com funções, há infinitos termos possíveis, como $f(a)$, $f(f(a))$ e assim por diante. Enumerar modelos como na tabela proposicional deixa de ser uma estratégia geral.

6. Unificação e encadeamento

Unificar duas expressões é encontrar uma substituição que as torne idênticas. Para

o unificador mais geral é

Ele é mais geral porque não faz substituições além das necessárias. A tentativa de unificar $x$ com $f(x)$ deve falhar pelo teste de ocorrência, ou occurs check. Aceitá-la exigiria um termo infinito $x=f(f(f(\ldots)))$.

Cláusulas de Horn têm no máximo um literal positivo e podem ser lidas como regras. O encadeamento para frente começa nos fatos e aplica regras cujos antecedentes já são conhecidos, até atingir um ponto fixo ou a consulta. O encadeamento para trás começa na meta, procura regras que poderiam concluí-la e transforma seus antecedentes em submetas.

Para os fatos $\operatorname{Pai}(\operatorname{joao},\operatorname{maria})$ e $\operatorname{Pai}(\operatorname{maria},\operatorname{ana})$, com a regra

a substituição ${x/\operatorname{joao},y/\operatorname{maria},z/\operatorname{ana}}$ deriva $\operatorname{Avo}(\operatorname{joao},\operatorname{ana})$.

Exercícios resolvidos

1. Unifique $P(x,f(y))$ e $P(a,f(g(z)))$.

Solução:

Igualamos os argumentos correspondentes: $x=a$ e $y=g(z)$. O MGU é ${x/a,y/g(z)}$.

2. Por que $x$ e $f(x)$ não unificam?

Solução:

$x$ ocorre dentro do termo que deveria substituí-lo. A substituição geraria uma estrutura infinita.

3. Unifique $Conhece(x,\operatorname{ana})$ e $Conhece(\operatorname{joao},y)$.

Solução:

O MGU é ${x/\operatorname{joao},y/\operatorname{ana}}$.

4. Prove que João é avô de Ana pelos fatos acima.

Solução:

A regra de avô unifica o primeiro antecedente com o primeiro fato e o segundo com o segundo fato, produzindo a conclusão desejada.

5. Quando o encadeamento para frente para?

Solução:

Quando deriva a consulta ou quando uma passagem completa não acrescenta fato novo. Como a base finita de fatos possíveis só cresce, esse ponto fixo termina no caso proposicional.

7. Verificação semântica e resolução em C++23

O programa representa um literal positivo pelo número da proposição e sua negação pelo oposto. A KB usa $p=1$, $q=2$ e $r=3$. Primeiro enumera os oito modelos e procura um contraexemplo para $r$. Depois acrescenta $\neg r$ e aplica resolução até encontrar $\square$. No MSVC 19.51, usamos cl /std:c++latest /permissive- /W4 /EHsc /utf-8 /O2 logica.cpp.

#include <algorithm>
#include <array>
#include <bitset>
#include <cstddef>
#include <cstdlib>
#include <iostream>
#include <ranges>
#include <vector>

using Literal = int;
using Clausula = std::vector<Literal>;
using FormaConjuntiva = std::vector<Clausula>;

[[nodiscard]] bool valor(
    const Literal literal, const std::bitset<3>& modelo) {
    const std::size_t indice =
        static_cast<std::size_t>(std::abs(literal) - 1);
    return literal > 0 ? modelo[indice] : !modelo[indice];
}

[[nodiscard]] bool satisfaz(
    const Clausula& clausula, const std::bitset<3>& modelo) {
    return std::ranges::any_of(
        clausula, [&modelo](const Literal l) { return valor(l, modelo); });
}

[[nodiscard]] bool satisfaz(
    const FormaConjuntiva& formula, const std::bitset<3>& modelo) {
    return std::ranges::all_of(
        formula,
        [&modelo](const Clausula& c) { return satisfaz(c, modelo); });
}

void normalizar(Clausula& clausula) {
    std::ranges::sort(clausula);
    const auto novo_fim = std::ranges::unique(clausula).begin();
    clausula.erase(novo_fim, clausula.end());
}

[[nodiscard]] bool tautologica(const Clausula& clausula) {
    return std::ranges::any_of(clausula, [&clausula](const Literal l) {
        return std::ranges::find(clausula, -l) != clausula.end();
    });
}

[[nodiscard]] std::vector<Clausula> resolver_par(
    const Clausula& a, const Clausula& b) {
    std::vector<Clausula> resolventes;
    for (const Literal pivô : a) {
        if (std::ranges::find(b, -pivô) == b.end()) {
            continue;
        }
        Clausula resolvente;
        resolvente.reserve(a.size() + b.size());
        std::ranges::copy_if(
            a, std::back_inserter(resolvente),
            [pivô](const Literal l) { return l != pivô; });
        std::ranges::copy_if(
            b, std::back_inserter(resolvente),
            [pivô](const Literal l) { return l != -pivô; });
        normalizar(resolvente);
        if (!tautologica(resolvente)) {
            resolventes.push_back(std::move(resolvente));
        }
    }
    return resolventes;
}

[[nodiscard]] bool refutar(FormaConjuntiva clausulas) {
    for (;;) {
        FormaConjuntiva novas;
        for (std::size_t i = 0; i < clausulas.size(); ++i) {
            for (std::size_t j = i + 1; j < clausulas.size(); ++j) {
                for (Clausula resolvente :
                     resolver_par(clausulas[i], clausulas[j])) {
                    if (resolvente.empty()) {
                        return true;
                    }
                    const bool conhecida =
                        std::ranges::find(clausulas, resolvente)
                            != clausulas.end()
                        || std::ranges::find(novas, resolvente) != novas.end();
                    if (!conhecida) {
                        novas.push_back(std::move(resolvente));
                    }
                }
            }
        }
        if (novas.empty()) {
            return false;
        }
        std::ranges::move(novas, std::back_inserter(clausulas));
    }
}

int main() {
    const FormaConjuntiva kb{
        Clausula{1, 2}, Clausula{-2, 3}, Clausula{-1}};
    constexpr Literal consulta = 3;

    std::size_t modelos_kb = 0;
    bool implica = true;
    for (unsigned mascara = 0; mascara < 8; ++mascara) {
        const std::bitset<3> modelo{mascara};
        if (satisfaz(kb, modelo)) {
            ++modelos_kb;
            implica = implica && valor(consulta, modelo);
        }
    }

    FormaConjuntiva refutacao = kb;
    refutacao.push_back({-consulta});
    const bool clausula_vazia = refutar(std::move(refutacao));

    std::cout << "modelos da KB = " << modelos_kb << '\n';
    std::cout << "KB implica r por modelos? "
              << (implica ? "sim" : "nao") << '\n';
    std::cout << "resolucao derivou clausula vazia? "
              << (clausula_vazia ? "sim" : "nao") << '\n';

    return modelos_kb == 1 && implica && clausula_vazia ? 0 : 2;
}

Os dois métodos precisam concordar: a KB possui um único modelo, nele $r$ é verdadeiro, e a resolução deriva a cláusula vazia após acrescentar $\neg r$. A enumeração é uma referência semântica exponencial; a resolução é uma prova sintática que pode evitar muitos modelos, embora também tenha pior caso exponencial.

No laboratório, ative ou remova as premissas $p\to q$ e $q\to r$. A tabela destaca contraexemplos para $p\to r$. Uma única linha em que a base seja verdadeira e a consulta falsa basta para destruir a consequência.

8. Dizer, significar e concluir

Sintaxe torna sentenças manipuláveis; semântica diz quando são verdadeiras; consequência lógica relaciona modelos; inferência procura provas; resolução transforma prova em refutação; unificação encontra as substituições que conectam regras gerais a fatos particulares.

No próximo artigo, essas peças formarão uma máquina de aconselhamento: regras de produção, memória de trabalho, fatores de certeza e uma trilha que explica cada conclusão.

Acrônimos e Abreviações neste artigo

A seguir está a lista de todos os acrônimos e abreviações identificados no texto, organizados em ordem alfabética com o termo original em inglês e a tradução para o português:

Referências

LUGER, G. F. Artificial Intelligence: structures and strategies for complex problem solving. 6. ed. Albuquerque: University of New Mexico, 2009. Disponível em: https://www.cs.unm.edu/~luger/ai-final/. Acesso em: 24 jul. 2026.

MARTELLI, A.; MONTANARI, U. An efficient unification algorithm. ACM Transactions on Programming Languages and Systems, New York, v. 4, n. 2, p. 258–282, 1982. DOI: https://doi.org/10.1145/357162.357169. Acesso em: 24 jul. 2026.

MICROSOFT. Microsoft C/C++ language conformance by Visual Studio version. Redmond, 2026. Disponível em: https://learn.microsoft.com/en-us/cpp/overview/visual-cpp-language-conformance?view=msvc-170. Acesso em: 24 jul. 2026.

ROBINSON, J. A. A machine-oriented logic based on the resolution principle. Journal of the ACM, New York, v. 12, n. 1, p. 23–41, 1965. DOI: https://doi.org/10.1145/321250.321253. Acesso em: 24 jul. 2026.

RUSSELL, S.; NORVIG, P. Artificial Intelligence: a modern approach. 4. ed. Hoboken: Pearson, 2020. Disponível em: https://aima.cs.berkeley.edu/. Acesso em: 24 jul. 2026.

UNIVERSITY OF CALIFORNIA, BERKELEY. Introduction to Artificial Intelligence: logic. Berkeley, 2024. Disponível em: https://inst.eecs.berkeley.edu/~cs188/textbook/logic/. Acesso em: 24 jul. 2026.