Agentes lógicos e planejamento

Um agente baseado em conhecimento age com base em uma descrição de seu mundo. Sua base de conhecimento (BC) contém sentenças formais: fatos e regras iniciais, chamados axiomas, e informações acrescentadas durante a operação. A inferência conecta essas sentenças a conclusões que o agente nunca observou diretamente.

Conecte percepção e ação

TELL acrescenta uma sentença à BC. ASK solicita uma resposta sustentada por ela, já armazenada ou derivada. A cada passo de tempo, o agente registra sua percepção, pergunta qual ação tomar, registra a ação escolhida e a executa. Registrar ações é importante porque o raciocínio posterior precisa saber como o mundo mudou.

No nível de conhecimento, podemos dizer que um robô sabe que uma passagem está bloqueada e quer chegar a uma área de armazenamento. No nível de implementação, descrevemos estruturas de dados e procedimentos de inferência. Um projeto declarativo fornece fatos e regras; um projeto procedural escreve o comportamento diretamente em código. Um agente em funcionamento pode combinar os dois.

Entenda o mundo do wumpus

O mundo do wumpus é uma grade de 4 × 4. As coordenadas são [coluna, linha]; o agente começa em [1, 1] voltado para a direita. Há um wumpus, uma peça de ouro e uma probabilidade de poço de 0,2 em cada casa, exceto na inicial. Os poços e o wumpus permanecem no mesmo lugar. O mundo é discreto, determinístico e de agente único, mas parcialmente observável: sua disposição está oculta.

Uma brisa indica um poço em uma casa diretamente adjacente; um fedor indica o wumpus nessa posição. Casas diagonais não contam. O brilho marca ouro na casa atual, o choque indica uma parede e o grito indica a morte do wumpus em qualquer lugar da caverna. As ações são avançar, virar à esquerda, virar à direita, pegar, atirar e sair. O agente tem uma flecha; sair só é possível a partir de [1, 1]. Sair com o ouro rende 1000 pontos, morrer faz perder 1000, cada ação custa 1 e atirar custa mais 10.

Combine observações

Em [1, 1], a ausência de brisa descarta poços em [1, 2] e [2, 1]; a ausência de fedor descarta o wumpus nessas casas. Ambas são seguras. Em [2, 1], uma brisa indica um poço em [2, 2] ou [3, 1], pois a casa inicial não tem poço. A ausência de fedor descarta o wumpus em [2, 2] e [3, 1].

Em seguida, o agente visita [1, 2]. A ausência de brisa exclui um poço em [2, 2], portanto a disjunção anterior exige um poço em [3, 1]. Um fedor em [1, 2] situa o wumpus em [1, 3] ou [2, 2]. A observação anterior de ausência de fedor exclui [2, 2], restando [1, 3]. O agente estabeleceu que [2, 2] não contém nenhum dos perigos sem entrar nela.

Esse raciocínio depende tanto das percepções quanto das regras que as relacionam aos perigos. Uma casa não explorada é desconhecida quando a BC não sustenta nem sua segurança nem seu perigo. Não conseguir derivar o perigo é insuficiente para afirmar que ela é segura. Escolher entrar nessa casa exige uma decisão sobre o risco, além das consequências lógicas por si só.

A lógica proposicional fornece a um agente regras precisas para combinar afirmações de sim ou não. Um símbolo atômico nomeia uma afirmação completa, como P₁₂ para “há um poço em [1, 2]”. Um literal é um átomo ou sua negação. Sentenças maiores os combinam com ¬, ∧, ∨, ⇒ e ⇔.

Avalie os conectivos

Um modelo atribui verdadeiro ou falso a cada símbolo. Com n símbolos, há 2ⁿ atribuições. A negação inverte um valor de verdade; uma conjunção exige que ambos os lados sejam verdadeiros; uma disjunção inclusiva exige pelo menos um. Uma implicação é falsa apenas quando a premissa é verdadeira e a conclusão é falsa. Uma bicondicional exige valores de verdade iguais nos dois lados.

A ordem de precedência é ¬, ∧, ∨, ⇒, ⇔. Assim, ¬A ∧ B ⇒ C significa ((¬A) ∧ B) ⇒ C. Use parênteses quando o agrupamento pretendido puder não estar claro. Com A verdadeiro, B falso e C verdadeiro, (A ∨ B) ⇒ C é verdadeira, enquanto A ⇒ (B ∧ C) é falsa.

A implicação lógica estabelece uma restrição sobre valores de verdade, não uma causa. Uma premissa falsa torna a implicação verdadeira. Ela também não permite inverter o sentido: de “se a bateria está descarregada, o robô para”, a parada, por si só, não permite concluir que a bateria está descarregada.

Codifique os dois sentidos de uma regra

A regra da brisa na casa inicial é B₁₁ ⇔ (P₁₂ ∨ P₂₁). Ela diz que há uma brisa exatamente quando existe um poço vizinho. O sentido B₁₁ ⇒ (P₁₂ ∨ P₂₁) permite detectar um perigo a partir de uma brisa. O sentido inverso permite excluir poços a partir da ausência de brisa. Omiti-lo impede a inferência de ¬B₁₁ para ¬P₁₂ ∧ ¬P₂₁.

Cada casa precisa de sua própria regra proposicional. Codificar exatamente um wumpus entre 16 casas exige uma disjunção de pelo menos um, além de uma restrição de no máximo um para cada par. Há 16 × 15 / 2 = 120 pares distintos. Símbolos proposicionais não podem quantificar sobre casas, portanto regras gerais tornam-se muitas sentenças separadas.

Represente mudanças sem perder a persistência

Um fluente é um fato cuja verdade pode mudar. Um índice de tempo sobrescrito distingue seus valores: L₁₁⁰ registra a localização no tempo 0. Um axioma de efeito pode dizer que mover-se para a direita a partir de [1, 1] produz a localização [2, 1] no tempo 1 e remove a localização anterior. Ele deixa em aberto o que acontece com fatos não relacionados, como a posse da flecha. Descrever todos esses fatos que não mudam é o problema do quadro.

Um axioma de estado sucessor fornece uma regra completa de atualização por fluente: Fᵗ⁺¹ ⇔ (uma ação torna F verdadeiro) ∨ (Fᵗ ∧ nenhuma ação torna F falso). Para a flecha, HaveArrowᵗ⁺¹ ⇔ (HaveArrowᵗ ∧ ¬Shootᵗ). Sem uma ação que forneça outra flecha, ela permanece com o agente até o disparo e continua ausente depois dele.

Um agente precisa de um critério para decidir se uma conclusão é justificada. Consequência lógica, escrita BC ⊨ α, significa que α é verdadeira em todo modelo que satisfaz a BC. Um único mundo compatível em que α é falsa invalida essa consequência lógica.

Mantenha exatamente os modelos compatíveis

A verificação de modelos enumera atribuições, descarta aquelas que tornam falsa alguma sentença da BC e testa a consulta nas que restam. Suponha que a BC contenha A ∨ B e ¬A. Das quatro atribuições a A e B, apenas A falso, B verdadeiro satisfaz ambas as sentenças. B e ¬A são consequências lógicas da BC. A não é consequência lógica dela porque o modelo restante torna A falsa.

Na BC do wumpus, ¬P₁₁, B₁₁ ⇔ (P₁₂ ∨ P₂₁), B₂₁ ⇔ (P₁₁ ∨ P₂₂ ∨ P₃₁), ¬B₁₁ e B₂₁ usam sete símbolos. Há 128 atribuições. Exatamente três satisfazem a BC: P₁₂ e P₂₁ são falsas, enquanto P₂₂ e P₃₁ são, respectivamente, verdadeira/falsa, falsa/verdadeira ou verdadeira/verdadeira. Assim, ¬P₁₂ é consequência lógica da BC. P₂₂ varia entre os três modelos, portanto nem P₂₂ nem ¬P₂₂ é consequência lógica dela. Essas regras sobre poços, por si só, estabelecem a ausência de um poço, não a ausência do wumpus.

Diferencie os principais testes lógicos

P ∨ ¬P é válida; P ∧ ¬P é insatisfatível. P ⇒ Q e ¬P ∨ Q são equivalentes. A equivalência exige consequência lógica nos dois sentidos. A ∧ B tem A como consequência lógica, mas A permite modelos em que B é falsa, portanto a consequência lógica inversa não vale.

Transforme uma consulta em um teste de contradição

BC ⊨ α exatamente quando BC ∧ ¬α é insatisfatível. Acrescentar a consulta negada busca um mundo em que a BC é verdadeira e a consulta é falsa. Não encontrar nenhum demonstra a consequência lógica; encontrar um fornece um contramodelo. Equivalentemente, α ⊨ β exatamente quando α ⇒ β é válida. A validade de α pode ser testada verificando se ¬α é insatisfatível.

O conectivo ⇒ pertence ao interior de uma sentença. O símbolo ⊨ descreve uma relação entre sentenças e seus modelos. Da mesma forma, “não é consequência lógica” pode significar que a consulta está descartada ou que permanece desconhecida. Verifique se a negação é consequência lógica antes de escolher entre as duas possibilidades.

A enumeração é correta e completa para a lógica proposicional porque verifica exaustivamente um conjunto finito. A enumeração em profundidade leva tempo O(2ⁿ) e memória O(n); 50 símbolos já fornecem cerca de 1,13 × 10¹⁵ atribuições. A consequência lógica proposicional é co-NP-completa. Verifique também a consistência: toda sentença é consequência lógica de uma BC sem modelos, pois ela não tem modelo compatível que possa violar uma consulta.

Uma demonstração deriva uma consulta aplicando regras a sentenças já conhecidas. BC ⊢ α registra uma derivação; BC ⊨ α registra uma garantia semântica sobre os modelos. Um procedimento de demonstração correto conecta os dois: toda conclusão que ele deriva realmente decorre das premissas. Um procedimento completo pode derivar toda conclusão que seja consequência lógica dentro da linguagem a que se destina.

Aplique regras às suas premissas

Modus ponens parte de P ⇒ Q e P para obter Q. A eliminação da conjunção parte de P ∧ Q para obter qualquer um dos termos da conjunção. Se SensorOn ∧ Calibrated é conhecido e SensorOn ⇒ ReadingAvailable é conhecido, a eliminação da conjunção fornece SensorOn, e então Modus ponens fornece ReadingAvailable. Cada linha identifica as informações e a regra que a justificam.

Essas regras preservam a verdade, mas seu vocabulário restrito as torna incompletas como sistema de demonstração. De P, a sentença P ∨ Q decorre semanticamente, mas nenhuma das regras introduz ∨. Um conjunto de regras corretas ainda pode deixar de encontrar conclusões válidas.

Reescreva sem mudar o significado

Equivalências úteis podem ser aplicadas nos dois sentidos:

• Dupla negação: ¬¬P ≡ P.
• Implicação: P ⇒ Q ≡ ¬P ∨ Q.
• Contraposição: P ⇒ Q ≡ ¬Q ⇒ ¬P.
• Bicondicional: P ⇔ Q ≡ (P ⇒ Q) ∧ (Q ⇒ P).
• De Morgan: ¬(P ∨ Q) ≡ ¬P ∧ ¬Q, e ¬(P ∧ Q) ≡ ¬P ∨ ¬Q.
• Distribuição: P ∨ (Q ∧ R) ≡ (P ∨ Q) ∧ (P ∨ R), com a lei dual para ∧ sobre ∨.

A conjunção e a disjunção também permitem reagrupar e reordenar os termos. Essas reescritas revelam a estrutura útil de uma sentença sem acrescentar uma nova hipótese factual.

Para B₁₁ ⇔ (P₁₂ ∨ P₂₁) e ¬B₁₁, separe a bicondicional e selecione (P₁₂ ∨ P₂₁) ⇒ B₁₁. A contraposição fornece ¬B₁₁ ⇒ ¬(P₁₂ ∨ P₂₁). Modus ponens fornece ¬(P₁₂ ∨ P₂₁); De Morgan fornece ¬P₁₂ ∧ ¬P₂₁. A eliminação da conjunção então demonstra ¬P₁₂. A demonstração nunca precisa enumerar todas as disposições possíveis da caverna.

Teste um atalho inválido

De P ⇒ Q e Q, inferir P é afirmar o consequente. De P ⇒ Q e ¬P, inferir ¬Q é negar o antecedente. Ambos falham no modelo P falso, Q verdadeiro. Uma queda do servidor pode impedir o carregamento de uma página, mas uma falha de carregamento tem outras causas possíveis; a ausência de uma queda também não garante o sucesso.

Encontrar uma demonstração é um problema de busca. O estado inicial contém a BC; uma ação aplica uma regra de inferência e acrescenta sua conclusão; o estado objetivo contém a consulta. O comprimento da demonstração pode servir como custo do caminho. Selecionar sentenças relevantes evita gastar esforço com cadeias não relacionadas. A lógica clássica é monotônica: acrescentar premissas preserva consequências lógicas anteriores. Regras por padrão com exceções precisam de outro tratamento, pois informações posteriores podem retirar uma conclusão anterior obtida por padrão.

A resolução demonstra uma consequência lógica buscando uma contradição. Sua entrada está na forma normal conjuntiva (FNC): uma conjunção de cláusulas, cada uma sendo uma disjunção de literais. Uma cláusula de um literal é uma cláusula unitária. A cláusula vazia não tem nenhum literal que possa ser verdadeiro e representa a falsidade.

Converta sentenças em cláusulas

Primeiro, elimine ⇔ e ⇒. Depois, mova as negações para dentro com as leis de De Morgan e a eliminação de duplas negações. Por fim, distribua ∨ sobre ∧. Uma bicondicional pode, portanto, gerar várias cláusulas.

Para B₁₁ ⇔ (P₁₂ ∨ P₂₁), o primeiro sentido fornece ¬B₁₁ ∨ P₁₂ ∨ P₂₁. O inverso fornece ¬(P₁₂ ∨ P₂₁) ∨ B₁₁. Mover a negação para dentro e distribuir fornece ¬P₁₂ ∨ B₁₁ e ¬P₂₁ ∨ B₁₁. As três cláusulas são necessárias para a bicondicional completa.

Resolva um par complementar

De P ∨ A e ¬P ∨ B, a resolução deriva A ∨ B. Qualquer que seja o valor de P, pelo menos uma das partes restantes deve ser verdadeira. A resolução unitária usa uma cláusula de um único literal: P com ¬P ∨ B fornece B. Literais duplicados são eliminados por fatoração, portanto resolver A ∨ B com A ∨ ¬B fornece A.

Resolva exatamente um par complementar por vez. A ∨ B e ¬A ∨ ¬B são conjuntamente satisfatíveis quando A é verdadeira e B é falsa. Remover ambos os pares forneceria incorretamente a cláusula vazia. Resolver apenas o par de A produz B ∨ ¬B, uma tautologia que não acrescenta nenhuma restrição.

Refute a consulta negada

Para demonstrar BC ⊨ α, acrescente ¬α, converta a sentença combinada para FNC e derive novos resolventes. Chegar à cláusula vazia demonstra que não existe contramodelo.

Para a consulta sobre o poço ¬P₁₂, acrescente P₁₂. Resolva-a com ¬P₁₂ ∨ B₁₁ para obter B₁₁. Resolva esse resultado com a observação ¬B₁₁ para chegar à cláusula vazia. A demonstração estabelece a ausência do poço, não sua presença: o literal positivo do poço era uma consulta negada temporária.

Um segundo exemplo usa R ⇒ C, (C ∨ I) ⇒ G e R. As cláusulas em FNC são ¬R ∨ C, ¬C ∨ G, ¬I ∨ G e R. Acrescente ¬G. Ela se resolve com ¬C ∨ G para fornecer ¬C, que fornece ¬R usando a primeira cláusula. Resolver ¬R com R conclui a refutação. Nenhum fato sobre I foi necessário.

A resolução proposicional é correta e completa para refutação. Ela termina porque um número finito de símbolos permite um número finito de cláusulas distintas. Se o fechamento exaustivo não produzir uma nova cláusula nem uma contradição, a consulta não é consequência lógica da BC. Ela não precisa derivar diretamente toda sentença que seja consequência lógica: apenas de A, a resolução não constrói A ∨ B.

A distribuição pode expandir a FNC exponencialmente. Uma codificação de Tseitin introduz símbolos para subfórmulas e produz uma FNC de tamanho linear. A nova sentença é equissatisfatível com a original; ela não precisa ser logicamente equivalente no vocabulário ampliado. Preservar a satisfatibilidade basta para testes de contradição baseados em SAT.

Regras com uma conclusão positiva permitem um procedimento de inferência mais simples que a resolução geral. Uma cláusula definida tem exatamente um literal positivo; ¬A ∨ ¬B ∨ C é escrita A ∧ B ⇒ C. Um fato tem corpo vazio. Uma cláusula de Horn tem no máximo um literal positivo, incluindo uma cláusula de objetivo sem nenhum, como A ∧ B ⇒ Falso.

Deixe os fatos orientar as regras

O encadeamento para frente começa com fatos conhecidos. Quando todas as premissas de uma regra forem conhecidas, acrescente sua cabeça. Continue até a consulta aparecer ou até um ponto fixo em que nada seja acrescentado. Implementações eficientes mantêm uma agenda de novos fatos e uma contagem de premissas não satisfeitas por regra.

Considere PowerOn, FanSpinning e LoadLow como fatos. As regras são PowerOn ∧ FanSpinning ⇒ Cooling; Cooling ∧ LoadLow ⇒ TempNormal; PowerOn ⇒ LedLit; LedLit ∧ TempNormal ⇒ SystemOK; FanSpinning ⇒ NoiseHeard. Processar PowerOn permite derivar LedLit e satisfaz parcialmente a regra de resfriamento. FanSpinning permite derivar Cooling e NoiseHeard. Cooling junto com LoadLow fornece TempNormal, e então TempNormal junto com LedLit fornece SystemOK. NoiseHeard é uma conclusão adicional válida, embora a consulta não precisasse dela.

Deixe uma consulta escolher as regras

O encadeamento para trás começa com SystemOK. Sua regra exige LedLit e TempNormal. LedLit reduz-se ao fato conhecido PowerOn. TempNormal exige Cooling e LoadLow; Cooling exige PowerOn e FanSpinning. Toda folha é um fato, portanto a consulta tem sucesso. A regra sobre ruído nunca é examinada.

Para BCs de cláusulas definidas e consultas atômicas, ambos os métodos são corretos e completos com controle adequado da busca. O encadeamento para frente proposicional pode executar em tempo linear no tamanho da BC. Em seu ponto fixo, atribuir verdadeiro aos símbolos derivados e falso a todos os outros fornece um modelo das cláusulas definidas.

Trate ciclos sem perder respostas

A ⇒ B e B ⇒ A colocam um procedimento ingênuo de encadeamento para trás em um ciclo infinito. Um ramo pode parar quando seu objetivo já está na pilha de objetivos ativos. Subobjetivos bem-sucedidos podem ser armazenados em cache, mas uma falha causada por um ciclo é temporária. Com B ⇒ A, A ⇒ B, C ⇒ A e o fato C, uma tentativa inicial de demonstrar B enquanto A está ativo pode falhar. Depois de demonstrar A a partir de C, uma nova tentativa de B tem sucesso. Armazenar a primeira falha permanentemente faria perder a demonstração. A tabulação de respostas acompanha objetivos dependentes e os revisita quando surgem respostas.

O encadeamento depende da forma da regra. A ∨ B tem dois literais positivos, portanto não é uma cláusula de Horn. Junto com A ⇒ C e B ⇒ C, ela tem C como consequência lógica ao considerar as duas alternativas. Nenhuma regra definida é acionada apenas a partir da disjunção. A resolução geral pode demonstrar essa conclusão mesmo quando o encadeamento simples para.

Um resolvedor SAT busca uma atribuição que satisfaça todas as cláusulas de uma sentença em FNC. Um modelo retornado pode ser verificado diretamente. Um resultado insatisfatível descarta todas as atribuições. SAT é NP-completo, mas instâncias estruturadas muitas vezes admitem soluções muito mais rápidas que a enumeração exaustiva por tabela-verdade.

Reduza a busca com DPLL

DPLL é uma busca com retrocesso em profundidade com três atalhos. Um literal verdadeiro satisfaz toda a sua cláusula, enquanto uma cláusula inteiramente falsa encerra o ramo. Um símbolo puro ocorre com apenas um sinal entre as cláusulas não satisfeitas, portanto pode receber um valor que satisfaça essas ocorrências. Uma cláusula unitária tem apenas um literal restante que pode ser verdadeiro, ao qual deve ser atribuído verdadeiro. Repetir essas escolhas forçadas é a propagação unitária.

Considere (A), (¬A ∨ B), (¬B ∨ C ∨ D), (¬C ∨ ¬D), (D ∨ E). E é puro, portanto atribua a ele verdadeiro. A cláusula unitária A força A a ser verdadeiro, o que força B a ser verdadeiro. A restrição restante C ∨ D e a cláusula ¬C ∨ ¬D exigem que exatamente um entre C e D seja verdadeiro. Ramifique com C verdadeiro; a propagação força D a ser falso. A, B, C e E verdadeiros com D falso satisfazem todas as cláusulas.

Para (A ∨ B), (A ∨ ¬B), (¬A ∨ C), (¬A ∨ ¬C), ramifique em A. A falso força tanto B quanto ¬B; A verdadeiro força tanto C quanto ¬C. Ambos os ramos entram em conflito, portanto a sentença inteira é insatisfatível.

Aprenda com os conflitos

O aprendizado de cláusulas dirigido por conflitos (CDCL) estende essa busca. Uma cláusula aprendida bloqueia uma combinação responsável por um conflito. O retrocesso com salto ignora escolhas irrelevantes; a atividade das variáveis orienta a ramificação; reinícios mudam o caminho da busca; literais observados aceleram a propagação. As cláusulas aprendidas são justificadas pela fórmula, portanto preservam suas possíveis soluções.

Busque alterando uma atribuição completa

WalkSAT começa com uma atribuição completa aleatória. Ele escolhe uma cláusula não satisfeita e inverte uma variável nela, às vezes aleatoriamente e às vezes para deixar o maior número de cláusulas satisfeitas. Movimentos aleatórios ajudam a escapar de armadilhas locais. Começar com os cinco símbolos falsos no exemplo anterior deixa (A) e (D ∨ E) falsas. Inverter A corrige (A), mas torna (¬A ∨ B) falsa. Um movimento pode reparar uma cláusula enquanto prejudica outra.

Para testar consequência lógica, forneça BC ∧ ¬α. A insatisfatibilidade demonstra α; um modelo é um contraexemplo. Um encerramento do WalkSAT por limite de tempo deixa as duas possibilidades em aberto. Em grandes fórmulas 3-FNC aleatórias, a razão entre cláusulas e variáveis tem uma transição estimada perto de 4,26, com instâncias difíceis frequentemente próximas a ela. Esse é um padrão do conjunto de fórmulas, não um limite que decide uma fórmula individual. A estrutura das cláusulas e a estratégia do resolvedor também afetam a dificuldade.

A lógica de primeira ordem descreve objetos e suas relações. Em vez de dar a cada casa um símbolo independente, ela pode expressar uma regra para todas as casas: ∀s (Breezy(s) ⇔ ∃r (Adjacent(r, s) ∧ Pit(r))). Os quantificadores incorporam a generalidade à linguagem.

Separe objetos de afirmações

Uma constante nomeia um objeto, como Ada. Uma variável, como x, assume valores entre os objetos. Uma função associa objetos a um objeto: MotherOf(Ada) é um termo que se refere a alguém. Um predicado forma uma afirmação: Owns(Ada, Atlas) é verdadeira ou falsa. Um termo pode ser uma constante, uma variável ou uma função aplicada a termos.

Book(x) é uma sentença, não um objeto, portanto Owns(Ada, Book(x)) coloca o tipo errado de expressão em uma posição de argumento. A igualdade compara aquilo a que os termos se referem: MotherOf(Ada) = Clara diz que ambos os termos denotam o mesmo objeto.

Avalie uma sentença em um modelo

Um modelo de primeira ordem fornece um domínio não vazio e uma interpretação. Constantes denotam objetos do domínio, predicados denotam relações e funções fornecem saídas para cada tupla apropriada de objetos do domínio. Uma sentença universalmente quantificada deve valer para todo valor possível de sua variável; uma sentença existencial precisa de pelo menos uma testemunha.

Seja o domínio {a, b, k}; Ada nomeia a, Ben nomeia b e Atlas nomeia k. Person contém a e b, Book contém k, e Owns contém apenas (a, k). Owns(Ada, Atlas) é verdadeira. ∃x (Book(x) ∧ Owns(Ben, x)) é falsa porque Ben não possui nenhum objeto. ∀x (Person(x) ⇒ ∃y (Book(y) ∧ Owns(x, y))) é falsa porque Ben é um contraexemplo. Ainda assim, todo livro tem um dono: ∀x (Book(x) ⇒ ∃y Owns(y, x)) vale.

Explicite as hipóteses de modelagem

A lógica de primeira ordem padrão não impõe essas hipóteses de banco de dados. Book(Atlas), Book(Beowulf), Owns(Ada, Atlas) e Owns(Ada, Beowulf) deixam em aberto se os dois nomes denotam o mesmo livro e se Ada possui mais livros. Sob a semântica de banco de dados, eles descrevem exatamente dois livros pertencentes a Ada.

Para obter essa afirmação exata na semântica padrão, mantenha os quatro fatos e acrescente ¬(Atlas = Beowulf) e ∀x ((Book(x) ∧ Owns(Ada, x)) ⇒ (x = Atlas ∨ x = Beowulf)). A desigualdade estabelece dois livros distintos; a restrição universal exclui outros livros que Ada possua.

Modelos de primeira ordem podem ter domínios arbitrariamente grandes, portanto o método de enumeração finita dos modelos proposicionais não fornece aqui um procedimento geral de decisão. Métodos de demonstração trabalham com a estrutura das sentenças. Uma variável livre precisa de uma atribuição para ser avaliada; vincule as variáveis ao escrever uma afirmação fechada para a BC.

A tradução começa decidindo o que a sentença afirma sobre cada objeto. O escopo dos quantificadores, o sentido da implicação e a igualdade determinam o significado; nomes de predicados, por si só, não o definem. Parênteses tornam o escopo pretendido visível.

Use o conectivo certo com um quantificador

“Todo gato é mamífero” torna-se ∀x (Cat(x) ⇒ Mammal(x)). Um objeto fora da categoria satisfaz a implicação sem ser gato. Escrever ∀x (Cat(x) ∧ Mammal(x)) faz com que tudo seja gato, incorretamente.

“Algum gato é preto” torna-se ∃x (Cat(x) ∧ Black(x)). A testemunha deve satisfazer ambas as propriedades. Com ∃x (Cat(x) ⇒ Black(x)), qualquer objeto que não seja gato já é uma testemunha, mesmo em um mundo sem gatos pretos. Regras universais de categoria geralmente usam implicação; afirmações existenciais sobre categorias geralmente usam conjunção.

Verifique quem pode depender de quem

∀x ∃y Loves(x, y) permite uma pessoa amada diferente para cada x. ∃y ∀x Loves(x, y) exige uma pessoa amada por todos. Em um mundo de duas pessoas no qual cada uma ama apenas a outra, a primeira vale e a segunda falha. Trocar a ordem de quantificadores de tipos diferentes pode mudar uma afirmação; trocar dois quantificadores universais adjacentes ou dois quantificadores existenciais adjacentes a preserva.

A negação troca os quantificadores: ¬∀x P(x) ≡ ∃x ¬P(x), e ¬∃x P(x) ≡ ∀x ¬P(x). Portanto, “Nem todo estudante foi aprovado” significa ∃x (Student(x) ∧ ¬Passed(x)). Isso exige um estudante que não foi aprovado; não afirma que todos os estudantes não foram aprovados.

Expresse sentido e quantidade

“Somente membros tomam emprestado” significa ∀x (Borrows(x) ⇒ Member(x)). Tomar emprestado basta para estabelecer o pertencimento, enquanto pertencer, por si só, nada diz sobre tomar emprestado. “Nenhum réptil é mamífero” significa ∀x (Reptile(x) ⇒ ¬Mammal(x)).

Para expressar que Ada possui pelo menos dois livros, escreva ∃x ∃y (Book(x) ∧ Book(y) ∧ Owns(Ada, x) ∧ Owns(Ada, y) ∧ ¬(x = y)). A desigualdade importa: dois nomes de variável podem referir-se ao mesmo objeto. Exatamente um usa uma testemunha e a unicidade: ∃x (Book(x) ∧ Owns(Ada, x) ∧ ∀y ((Book(y) ∧ Owns(Ada, y)) ⇒ y = x)).

Dê os dois sentidos às definições

Uma definição de irmãos pode ser ∀x ∀y (Sibling(x, y) ⇔ (¬(x = y) ∧ ∃p (Parent(p, x) ∧ Parent(p, y)))). O primeiro sentido impõe condições aos irmãos; o inverso permite que fatos sobre compartilhar um dos pais estabeleçam que duas pessoas são irmãos. Uma implicação em um único sentido fornece apenas metade desse significado.

Em um domínio de agente, regras diagnósticas vão das observações às possíveis causas, enquanto regras causais vão das causas aos efeitos. “Toda casa com brisa tem um poço adjacente” é diagnóstica. “Todo poço faz com que toda casa adjacente tenha brisa” é causal. Juntas, elas sustentam a bicondicional completa da brisa. Termine uma tradução verificando a vinculação de cada variável e testando um pequeno mundo no qual a afirmação em português deveria ser falsa.

Construir uma base de conhecimento útil é uma tarefa de modelagem. A notação formal só ajuda depois que as perguntas, os objetos e as relações relevantes foram escolhidos. A engenharia do conhecimento transforma essas escolhas em axiomas que podem ser verificados com exemplos pretendidos.

Construa em torno das perguntas

Uma sequência prática é identificar a tarefa, reunir o conhecimento relevante, escolher um vocabulário, escrever axiomas gerais, acrescentar fatos da instância, fazer consultas e corrigir os resultados. Comece com perguntas concretas como “Este estudante pode se matricular nesta disciplina?”. Essa pergunta determina o que a representação deve permitir responder.

Para matrícula, use Student(s), Course(c), Prereq(p, c), Passed(s, c) e CanEnroll(s, c). Prereq(p, c) significa que é preciso ser aprovado em p antes de cursar c; inverter seus argumentos inverteria a dependência. Uma regra é ∀s ∀c ((Student(s) ∧ Course(c) ∧ ∀p (Prereq(p, c) ⇒ Passed(s, p))) ⇒ CanEnroll(s, c)). Ela exige todos os pré-requisitos, não apenas um.

Separe regras reutilizáveis de uma instância

Suponha que os fatos sejam Student(Mia), Course(AI), Prereq(Logic, AI), Prereq(Programming, AI), Passed(Mia, Logic) e Passed(Mia, Programming). A regra geral pode ser reutilizada para outros estudantes e disciplinas, enquanto esses fatos da instância descrevem um caso.

Na lógica de primeira ordem padrão, esses fatos deixam em aberto a existência de pré-requisitos adicionais para AI. Um modelo compatível poderia incluir um terceiro pré-requisito no qual Mia não foi aprovada, portanto CanEnroll(Mia, AI) ainda não é consequência lógica da BC. Acrescente ∀p (Prereq(p, AI) ⇔ (p = Logic ∨ p = Programming)) para completar a lista. Agora cada pré-requisito é uma das duas disciplinas nas quais ela foi aprovada, e a regra de matrícula se aplica. Um banco de dados de mundo fechado pode obter a mesma resposta tratando fatos ausentes sobre pré-requisitos como falsos.

Escolha o que se torna um objeto

Uma ontologia é o vocabulário e suas hipóteses estruturais. Red(x) trata o vermelho como propriedade. Color(x, Red) faz de Red um objeto, permitindo que ∃c (Color(x, c) ∧ Color(y, c)) expresse uma cor compartilhada. Essa mudança é a reificação: ela permite que a linguagem trate uma propriedade ou categoria como algo por si só.

ASK pode perguntar se CanEnroll(Mia, AI) é consequência lógica da BC. ASKVARS pode solicitar vinculações para CanEnroll(x, AI), retornando uma substituição como {x/Mia}. A mesma BC permite tanto perguntas sobre a verdade quanto consultas por objetos correspondentes.

Corrija o significado, não apenas a sintaxe

Um axioma ausente pode impedir uma consequência lógica desejada; um axioma incorreto pode sustentar uma consequência indesejada. Teste exemplos positivos, exemplos negativos e casos-limite. A regra ∀c (Course(c) ⇒ ∃t Teaches(t, c)) é forte demais se algumas disciplinas ainda não têm professor. A regra ∀p ∀c (Prereq(p, c) ⇒ Passed(Mia, p)) é forte demais porque atribui a Mia a aprovação em todos os pré-requisitos de todas as disciplinas.

Nomes de predicados são rótulos para o sistema de raciocínio. Chamar uma relação de Prereq não fornece, por si só, uma política de matrícula. As regras devem conectar fatos sobre pré-requisitos, disciplinas concluídas e elegibilidade no sentido pretendido.

A inferência de primeira ordem trabalha com padrões que contêm variáveis. A substituição troca variáveis por termos; a unificação encontra substituições que tornam duas expressões idênticas. Juntas, elas permitem que uma regra geral atenda a muitos fatos específicos sem gerar primeiro todas as instâncias possíveis.

Instancie sentenças quantificadas com cuidado

A instanciação universal substitui uma variável universalmente vinculada por qualquer termo sem variáveis. De ∀x (Cat(x) ⇒ Mammal(x)), derive Cat(Tom) ⇒ Mammal(Tom), ou a instância correspondente com MotherOf(Tom). Um termo sem variáveis não contém nenhuma variável.

A instanciação existencial introduz um novo nome para uma testemunha. De ∃x (Crown(x) ∧ OnHead(x, John)), introduza uma nova constante C₁ e acrescente Crown(C₁) e OnHead(C₁, John). Nomear Ben como testemunha identificaria incorretamente um objeto não especificado com um objeto existente. A BC ampliada preserva a satisfatibilidade, mas não a equivalência no vocabulário ampliado.

A proposicionalização gera instâncias sem variáveis e então usa raciocínio proposicional. Símbolos de função podem produzir infinitos termos: Ada, MotherOf(Ada), MotherOf(MotherOf(Ada)) e assim por diante. Consultas de primeira ordem que são consequências lógicas têm demonstrações finitas, mas um demonstrador geral pode executar indefinidamente quando a consulta não é consequência lógica. Isso é semidecidibilidade.

Encontre uma substituição consistente

Para unificar Knows(Ana, x) com Knows(y, Bo), primeiro faça corresponder o predicado e a aridade. Os primeiros argumentos exigem y = Ana; os segundos exigem x = Bo. A substituição {y/Ana, x/Bo} torna ambas as expressões iguais a Knows(Ana, Bo).

Knows(Ana, x) e Knows(y, MotherOf(y)) fornecem {y/Ana, x/MotherOf(Ana)}. Uma vinculação deve ser propagada pelos outros termos. Se a mesma variável x ocorre nas duas expressões Knows(Ana, x) e Knows(x, Bo), ela precisaria tornar-se Ana e Bo ao mesmo tempo, portanto a unificação sintática falha.

Variáveis em sentenças quantificadas separadamente são independentes. A padronização de variáveis à parte renomeia-as antes de combinar as sentenças. Renomear o segundo x como z nesse último par permite {z/Ana, x/Bo}. Isso preserva a independência pretendida das variáveis locais de duas regras.

Um unificador mais geral não impõe vinculações desnecessárias. Knows(Ana, x) e Knows(y, z) unificam-se com {y/Ana, x/z}; atribuir também Ana a z especializaria o resultado sem necessidade. A verificação de ocorrência rejeita x = MotherOf(x), pois um termo finito não pode conter a si mesmo. A unificação comum em Prolog pode permitir termos cíclicos, portanto seu comportamento exige cuidado quando se pretende usar lógica de primeira ordem com termos finitos.

Aplique a regra correspondente

O Modus ponens generalizado faz todas as premissas corresponderem sob uma única substituição consistente. Owns(Ada, Atlas) e Book(Atlas) correspondem a Owns(x, y) ∧ Book(y) ⇒ Reader(x) com {x/Ada, y/Atlas}, fornecendo Reader(Ada). Fazer uma premissa corresponder com y = Atlas e outra com y = Beowulf não justificaria acionar a regra: variáveis compartilhadas exigem objetos compartilhados.

Uma cláusula definida de primeira ordem tem premissas atômicas e uma conclusão atômica, com suas variáveis consideradas universalmente quantificadas. Os encadeamentos para frente e para trás usam unificação para aplicar essas regras a objetos nomeados. Datalog mantém essa forma de regra e exclui símbolos de função, produzindo um espaço finito de fatos possíveis sem variáveis no contexto usual de um banco de dados finito.

Derive locais alcançáveis

Considere Link(A, B), Link(B, C) e Link(C, D). Use Link(x, y) ⇒ Reach(x, y) e Link(x, y) ∧ Reach(y, z) ⇒ Reach(x, z). Em rodadas síncronas, cada regra lê os fatos disponíveis antes daquela rodada.

A rodada 1 deriva Reach(A, B), Reach(B, C) e Reach(C, D). A rodada 2 acrescenta Reach(A, C) e Reach(B, D). A rodada 3 acrescenta Reach(A, D). A rodada 4 não acrescenta nada. Há seis fatos Reach no ponto fixo. Uma implementação que reutiliza imediatamente novos fatos pode encontrá-los em outra ordem, mas chega ao mesmo fechamento.

Com n constantes e predicados de aridade no máximo k, apenas um número finito de tuplas é possível; um limite superior é p · nᵏ para p predicados. Em contraste, NatNum(0) e NatNum(n) ⇒ NatNum(S(n)) geram termos cada vez mais profundos indefinidamente. Símbolos de função eliminam a garantia de domínio finito.

Fazer corresponder uma regra com várias premissas é um problema de restrições. Uma premissa seletiva pode reduzir muito as substituições consideradas em seguida. O encadeamento para frente incremental concentra-se em regras afetadas por fatos recém-acrescentados. Redes Rete mantêm correspondências parciais entre atualizações, evitando trabalho repetido em sistemas de regras de produção.

Trabalhe para trás com vinculações

Para demonstrar Reach(A, D), tente a regra de vínculo direto, que exige o fato ausente Link(A, D). A regra recursiva exige Link(A, y) e Reach(y, D). A primeira vincula y a B. Continuar por B e C leva ao fato conhecido Link(C, D). A consulta Reach(A, w) tem três respostas: w = B, C ou D.

Prolog escreve regras com a cabeça primeiro e usa variáveis em maiúsculas e constantes em minúsculas:

reach(X, Y) :- link(X, Y).
reach(X, Z) :- link(X, Y), reach(Y, Z).

Ela tenta as cláusulas de cima para baixo e as premissas da esquerda para a direita, usando encadeamento para trás em profundidade. A aritmética pode usar N is M + 1. A negação por falha, escrita \+ p, tem sucesso se a tentativa de demonstrar p falhar em um número finito de passos. Ela é um teste operacional de falha, não uma demonstração geral de negação clássica.

Evite que a recursão prenda a busca

Colocar reach(X, Y) primeiro no corpo recursivo pode chamar imediatamente o mesmo objetivo ainda não resolvido. Colocar as cláusulas base primeiro e usar uma recursão que consome um vínculo ajuda, mas ciclos ainda podem prender buscas malsucedidas. A tabulação de respostas registra respostas de subobjetivos e gerencia dependências repetidas. O encadeamento para frente é completo para Datalog finito; a busca ingênua para trás em profundidade precisa desse tipo de controle para evitar perder respostas alcançáveis atrás de ramos infinitos.

A resolução de primeira ordem amplia o raciocínio com cláusulas por meio da unificação. Ela pode demonstrar conclusões que envolvem objetos sem nome porque os termos de Skolem preservam as dependências das testemunhas existenciais. Como na refutação proposicional, comece com a BC e a negação da consulta.

Prepare cláusulas de primeira ordem

Elimine ⇔ e ⇒, mova as negações para dentro, padronize as variáveis vinculadas, Skolemize as existenciais, elimine os quantificadores universais e distribua ∨ sobre ∧. Mover a negação primeiro é importante porque ¬∀x P(x) torna-se ∃x ¬P(x), mudando o tipo de testemunha necessário.

Para “Toda disciplina tem um professor”, ∀c (Course(c) ⇒ ∃t Teaches(t, c)), o professor existencial pode depender de c. Introduza uma nova função T(c) para obter ¬Course(c) ∨ Teaches(T(c), c). Uma única constante imporia um professor comum, o que a sentença original não exige. Para ∃t ∀c (Course(c) ⇒ Teaches(t, c)), uma nova constante é apropriada porque a testemunha precede o quantificador universal.

“Nem toda ave voa” torna-se ∃x (Bird(x) ∧ ¬Flies(x)) e depois Bird(B₁) e ¬Flies(B₁). Ambas as cláusulas usam a mesma nova testemunha. A Skolemização preserva a satisfatibilidade; ela não é uma equivalência comum no vocabulário ampliado.

Aplique um unificador a todo o resolvente

Padronize as variáveis das duas cláusulas à parte. Encontre literais complementares que se unifiquem, remova-os e aplique seu unificador mais geral a cada literal restante. A fatoração também combina literais unificáveis dentro de uma cláusula. A resolução com fatoração é completa para refutação de cláusulas de primeira ordem.

Considere ¬Course(c) ∨ Teaches(T(c), c), ¬Teaches(u, v) ∨ Staff(u) e Course(Logic). A consulta é ∃w Staff(w); sua negação fornece ¬Staff(w), universalmente quantificada. Resolva o fato sobre a disciplina com a primeira cláusula para obter Teaches(T(Logic), Logic). Resolva com a segunda sob {u/T(Logic), v/Logic}, obtendo Staff(T(Logic)). Resolva com ¬Staff(w) sob {w/T(Logic)} para chegar à cláusula vazia. Existe um membro da equipe, embora a BC nunca dê a essa pessoa um nome comum.

Controle a busca por cláusulas

A preferência unitária escolhe primeiro cláusulas curtas. O conjunto de suporte exige uma cláusula de origem da consulta negada ou de suas descendentes e preserva a completude quando o restante da BC é satisfatível. A resolução de entrada exige uma cláusula de origem original em cada passo e é completa para BCs de Horn. A subsunção remove uma cláusula mais fraca já abrangida por uma mais forte e geral, como ao excluir P(Ana) ∨ Q(Bo) quando P(x) é conhecida.

A igualdade precisa de tratamento específico: axiomas de igualdade, reescrita por equações por meio de demodulação ou inferências como a paramodulação. A resolução puramente sintática, por si só, não captura todos os significados da igualdade. Uma busca justa e completa encontra uma contradição para todo conjunto insatisfatível de cláusulas de primeira ordem, mas pode executar indefinidamente nos demais casos. Demonstradores baseados em resolução incluem Vampire e E; EQP demonstrou a conjectura de Robbins em 1996.

Uma ontologia organiza as categorias, os objetos, as relações e as hipóteses de um domínio. Uma ontologia superior fornece ideias amplas, como objetos, eventos e tempo; uma ontologia de domínio fornece as distinções úteis em uma área específica. Ontologias clínicas e biológicas ilustram por que um vocabulário compartilhado útil frequentemente atende a uma comunidade específica.

Mantenha pertencimento e subclasse separados

Uma categoria pode aparecer como predicado, Laptop(x), ou como objeto, Laptops. O pertencimento x ∈ Laptops diz que um indivíduo pertence a ela. Laptops ⊂ Computers diz que todo notebook é um computador. Uma taxonomia organiza essas relações de subclasse em uma hierarquia. Se todo computador tem um processador, notebooks herdam essa propriedade.

A relação de subclasse é transitiva: Penguins ⊂ Birds e Birds ⊂ Animals fornecem Penguins ⊂ Animals. O pertencimento não é transitivo. Pingu ∈ Penguins e Penguins ∈ Species não fazem de Pingu uma espécie. Uma afirmação diz respeito a uma ave individual; a outra diz respeito a uma categoria tratada como objeto.

Categorias são disjuntas quando não compartilham membros. Uma decomposição exaustiva abrange todo membro da categoria superior. Uma partição faz as duas coisas: inteiros negativos, zero e inteiros positivos particionam os inteiros. A exaustividade permite sobreposição, a menos que a disjunção também seja afirmada.

Represente partes, eventos e valores herdados

PartOf descreve composição, não pertencimento a uma categoria. PartOf é transitiva: um raio que pertence a uma roda que pertence a uma bicicleta é parte da bicicleta. Isso não faz de uma bicicleta um tipo de roda. Eventos também podem ser objetos: Happens(e, t), Initiates(e, f, t) e HoldsAt(f, t) conectam eventos a fluentes que mudam. Acender uma lâmpada inicia um fluente que persiste até que um evento o encerre.

Uma rede semântica representa objetos e categorias como nós com relações rotuladas. Em uma rede com padrões, “aves normalmente voam” pode fornecer um valor herdado por aves comuns, enquanto uma categoria mais específica de pinguins o substitui. Isso é diferente de afirmar o axioma clássico sem exceções ∀x (Bird(x) ⇒ Flies(x)), que também se aplicaria aos pinguins.

Escolha a linguagem de raciocínio

Lógicas de descrição permitem verificar subsunção, classificação e consistência. Uma definição pode classificar uma pessoa com pelo menos três filhos em uma categoria apropriada. Essas lógicas formam a base das linguagens de lógica de descrição de OWL.

O raciocínio por padrão é não monotônico: saber que uma ave é um pinguim pode retirar uma conclusão padrão de que ela voa. A circunscrição minimiza casos anormais em regras como Bird(x) ∧ ¬Abnormal(x) ⇒ Flies(x). A lógica de padrões permite conclusões enquanto elas permanecem consistentes com o conhecimento. Sistemas de manutenção da verdade registram o suporte para que conclusões que dependam de uma crença retirada possam ser removidas.

Um grafo de conhecimento armazena entidades e suas relações como um grafo direcionado. Uma aresta simples torna-se uma tripla: sujeito, predicado, objeto. Por exemplo, (Ada, worksAt, Lab) corresponde a WorksAt(Ada, Lab); (Ada, type, Researcher) afirma o pertencimento a uma categoria. Um esquema dá significado compartilhado a esses rótulos e permite novas inferências.

Diferencie os padrões da web

RDF representa grafos como triplas. Sujeitos são IRIs ou nós em branco, predicados são IRIs e objetos também podem ser valores literais. IRIs identificam recursos em diferentes conjuntos de dados; um nó em branco representa um recurso sem lhe dar um identificador global. RDFS acrescenta classes, relações de subclasse e domínio e imagem de propriedades. OWL fornece definições de ontologia mais ricas. SPARQL faz a correspondência de padrões de grafo para retornar vinculações de variáveis. Grafos de propriedades oferecem outro modelo com propriedades de chave–valor em nós e arestas; Cypher e GQL são linguagens de consulta dessa família.

Se Ada é classificada como Researcher e Researcher é uma subclasse de Scientist, uma regra de subclasse deriva que Ada é Scientist. Isso é encadeamento para frente de primeira ordem sobre Member(x, c) ∧ Subset(c, d) ⇒ Member(x, d). Um mecanismo de consulta de grafos precisa do suporte relevante à consequência lógica ou de conclusões materializadas para apresentar esse fato inferido.

Faça a correspondência de uma consulta e preserve os detalhes

Com ex: declarado como prefixo de IRI, uma consulta pode ser:

SELECT ?p WHERE {
  ?p a ex:Researcher .
  ?p ex:worksAt ex:Lab .
}

O mesmo ?p deve satisfazer ambos os padrões. É uma junção, não duas buscas independentes. Os resultados são vinculações como ?p = ex:Ada, semelhantes às substituições em consultas lógicas.

Uma aresta binária não pode, por si só, expressar todos os papéis em um evento com data. Para um prêmio, crie um nó de evento ou de afirmação e conecte-o ao destinatário, ao prêmio e ao ano. Isso mantém juntos os detalhes de um prêmio e evita associar acidentalmente a data a todos os prêmios desse tipo. O Wikidata permite qualificadores de afirmação para esses detalhes.

Separe vínculos ausentes, inferidos e previstos

RDF e OWL usam uma leitura de mundo aberto: uma aresta ausente sobre o cônjuge deixa a relação desconhecida. Aplicações de mundo fechado fazem uma escolha diferente sobre fatos ausentes. Um resultado vazio de consulta informa a ausência de correspondência naquela configuração de consulta; por si só, ele não estabelece um fato negativo universal.

Wikidata, DBpedia, Knowledge Graph do Google e grafos internos de organizações apoiam consultas factuais, vinculação de registros, recomendações e recuperação de informações para sistemas generativos. Seus fatos podem estar incompletos ou desatualizados. A resolução de entidades identifica registros que se referem à mesma coisa mesmo quando os identificadores são diferentes.

Representações vetoriais atribuem vetores a entidades e relações. No TransE, o vetor da cabeça somado ao vetor da relação é treinado para ficar próximo do vetor da cauda. Uma pontuação alta sugere um vínculo ausente; é uma previsão estatística. A inferência lógica deriva uma consequência de fatos e regras declarados. Mantenha essa diferença visível ao decidir se uma nova aresta pertence ao conjunto de fatos verificados.

O planejamento clássico busca ações que levem um estado inicial conhecido a um objetivo. O modelo é totalmente observável, determinístico, discreto e de agente único; o mundo muda por meio das ações modeladas. Uma representação fatorada descreve cada estado por meio de fluentes, para que um planejador possa raciocinar sobre o que cada ação altera.

Escreva o estado e os esquemas de ação

No fragmento básico de PDDL no estilo STRIPS, um estado lista fluentes atômicos verdadeiros sem variáveis. Fluentes não listados são falsos sob a hipótese de mundo fechado. O domínio reutilizável declara predicados e esquemas de ação; o problema declara objetos, o estado inicial e um objetivo. PDDL foi introduzida para a competição de planejamento de 1998, com base em STRIPS.

Um esquema de ação tem parâmetros, uma precondição e efeitos. Go(r, from, to) exige At(r, from) e Connected(from, to); adiciona At(r, to) e remove At(r, from). Pick(r, p, l) exige At(r, l), In(p, l) e HandEmpty(r); adiciona Holding(r, p) e remove In(p, l) e HandEmpty(r). Drop exige localização e posse; adiciona a localização do pacote e uma mão vazia e remove a posse.

Uma ação sem variáveis só se aplica quando suas precondições são verdadeiras. Sua atualização é RESULT(s, a) = (s − DEL(a)) ∪ ADD(a). Outros fluentes persistem, incluindo fatos estáticos Connected. Essa persistência implícita trata o problema do quadro sem um axioma separado para cada fluente não afetado.

Acompanhe uma entrega em quatro ações

Inicialmente, R está em Dock, Box está em Shelf e a mão de R está vazia. Vínculos Connected ligam Dock a Shelf e Shelf a Packing nos dois sentidos. O objetivo é In(Box, Packing).

1. Go(R, Dock, Shelf) altera a localização de R e preserva os fatos sobre a caixa e a mão.
2. Pick(R, Box, Shelf) remove a caixa da prateleira e faz R segurá-la.
3. Go(R, Shelf, Packing) move R preservando Holding(R, Box).
4. Drop(R, Box, Packing) coloca a caixa em Packing e libera a mão.

O objetivo deixa a localização final do robô não especificada, exceto onde as ações a exigem. Objetivos geralmente descrevem muitos estados aceitáveis, não um único estado completo.

Leia e verifique um esquema

(:action pick
 :parameters (?r ?p ?l)
 :precondition (and (at ?r ?l) (in ?p ?l) (hand-empty ?r))
 :effect (and (holding ?r ?p)
              (not (in ?p ?l)) (not (hand-empty ?r))))

Omitir um efeito de remoção pode deixar um robô em dois lugares ou um pacote sendo segurado e sobre uma prateleira ao mesmo tempo. Colocar uma condição necessária apenas em um efeito faz a ação criá-la em vez de verificá-la.

No mundo dos blocos, mover um bloco livre b de x para cima de um bloco livre y exige On(b, x), Clear(b), Clear(y), Block(b), Block(y) e ¬(b = y). A ação adiciona On(b, y) e Clear(x), e remove On(b, x) e Clear(y). As verificações de distinção e de bloco impedem empilhar um bloco sobre si mesmo e tratar a mesa como um único bloco. Uma ação separada MoveToTable mantém a mesa disponível para outros blocos.

Um modelo de planejamento define um espaço de busca, mas escolher ações úteis ainda é difícil. A progressão busca para frente por estados completos. A regressão busca para trás pelas condições que um estado anterior deve satisfazer. Ambas podem reutilizar métodos gerais de busca e aproveitar a estrutura das ações.

Busque a partir de qualquer uma das pontas

A progressão começa no estado inicial e aplica ações aplicáveis sem variáveis. Ela pode desperdiçar esforço com ações irrelevantes: um robô, 20 caixas e 10 locais já fornecem 200 combinações possíveis de Pick sem variáveis antes da filtragem por aplicabilidade.

A regressão considera uma ação que alcança um literal do objetivo sem negar outro literal do objetivo. Para regredir um conjunto de objetivos g por a, remova os literais alcançados e acrescente as precondições: g′ = (g − EFFECT(a)) ∪ PRECOND(a). EFFECT inclui literais positivos e negativos com seus sinais. Rejeite um resultado inconsistente que contenha um literal e sua negação.

Para In(Box, Packing) ∧ At(R, Dock), regredir por Drop(R, Box, Packing) fornece Holding(R, Box) ∧ At(R, Packing) ∧ At(R, Dock). Essas condições entram em conflito com a invariante pretendida de localização única. Um plano válido deve entregar a caixa antes do retorno final do robô. Regredir por Go(R, Shelf, Dock), por sua vez, fornece In(Box, Packing) ∧ At(R, Shelf) ∧ Connected(Shelf, Dock), preservando o pacote entregue.

Estime a distância usando problemas mais simples

Uma heurística é admissível quando nunca superestima o custo ótimo restante. A* com uma heurística admissível encontra um plano ótimo. Contar objetivos não satisfeitos nem sempre é admissível: uma única ação pode alcançar vários.

Ignorar precondições torna todas as ações imediatamente utilizáveis. Ignorar efeitos de remoção torna o progresso permanente, em problemas expressos com precondições e objetivos positivos. Condições negativas devem primeiro ser convertidas em fluentes positivos mantidos explicitamente. O comprimento ótimo do plano relaxado h⁺ é um limite inferior para o comprimento do plano real, mas calculá-lo é NP-difícil. FF encontra rapidamente um plano relaxado sem garantir sua otimalidade; seu comprimento pode superestimar h⁺ e não tem garantia de ser admissível.

Para o objetivo de entrega e retorno no armazém, o plano real de menor comprimento tem seis ações: ir a Shelf, pegar, ir a Packing, soltar, voltar a Shelf e voltar a Dock. O relaxamento por desconsideração de efeitos de remoção precisa apenas das quatro primeiras porque At(R, Dock) permanece verdadeiro após a saída. Assim, h⁺ = 4 enquanto o custo real é 6. A contagem de objetivos não satisfeitos começa em apenas 1 e deixa passar a maior parte desse trabalho.

Combine estimativas sem contar duas vezes

Um grafo de planejamento alterna níveis de fluentes e de ações possíveis, com vínculos de exclusão mútua marcando pares incompatíveis. A primeira aparição de um objetivo fornece uma estimativa por nível. Usar o máximo dos níveis individuais dos objetivos é admissível; somá-los pode contar repetidamente o trabalho compartilhado. A abstração de estados remove alguns fluentes para reduzir o espaço de estados. A decomposição em subobjetivos também se beneficia da verificação de ações compartilhadas: o máximo dos custos admissíveis dos subobjetivos é seguro, enquanto sua soma precisa de justificativa adicional.

Métodos de planejamento diferem no que exploram: estados, atribuições de valores de verdade, restrições de ordenação ou refinamentos de procedimentos de especialistas. Sua utilidade depende da interação entre subobjetivos e das hipóteses que o modelo faz sobre a execução.

Reconheça subobjetivos que interagem

Na anomalia de Sussman, C está sobre A, com A e B sobre a mesa. O objetivo é On(A, B) ∧ On(B, C). Concluir primeiro o subobjetivo de colocar A sobre B bloqueia a colocação posterior de B. Colocar B sobre C imediatamente deixa A preso embaixo. Um plano de menor comprimento libera A primeiro e depois constrói a pilha de baixo para cima: mover C para a mesa, mover B para cima de C e então mover A para cima de B. Os três movimentos intercalam preparação e alcance de objetivos.

Codifique um plano limitado como SAT

SATPlan escolhe um horizonte T. Ele afirma os fluentes iniciais no tempo 0, os fluentes do objetivo em T, as precondições das ações, as restrições de estado sucessor e as exclusões para ações incompatíveis. Uma atribuição satisfatória seleciona ações que formam um plano. Um resultado insatisfatível exclui planos dentro dessa codificação e desse horizonte.

Tentar horizontes em ordem encontra o menor horizonte satisfatível. Com ações paralelas, isso minimiza camadas, não necessariamente o número total de ações. É necessário um limite de parada para transformar horizontes insatisfatíveis repetidos na conclusão de que não existe plano.

Mantenha apenas a ordem necessária

O planejamento de ordem parcial registra ações, restrições de ordem e vínculos causais. Um vínculo de A para B, identificado por p, diz que A estabelece a precondição p de B. Uma ação C que poderia remover p entre elas é uma ameaça. O rebaixamento ordena C antes de A; a promoção a ordena depois de B. Ações não relacionadas podem permanecer sem ordem definida até a execução, seguindo o compromisso mínimo.

O planejamento HTN refina tarefas de alto nível por meio de uma biblioteca de métodos. DeliverBox pode tornar-se viajar até a caixa, pegá-la, viajar ao destino e soltá-la. Esses métodos codificam procedimentos de especialistas, portanto a busca pode se concentrar em refinamentos úteis em vez de considerar cada ação primitiva a cada ponto.

Ajuste o modelo ao mundo

A existência de plano para STRIPS proposicional geral é PSPACE-completa. O mundo dos blocos tem um problema de existência mais fácil para disposições possíveis: mova os blocos para a mesa e reconstrua as pilhas, usando no máximo 2n movimentos para n blocos. Encontrar um plano de menor comprimento para o mundo dos blocos ainda é NP-difícil.

Modelos clássicos deixam de fora resultados incertos, estado oculto e durações das ações. Planos conformantes funcionam sem observações, planos contingentes ramificam-se conforme as observações, o replanejamento em tempo de execução responde a diferenças durante a execução, e a programação de tarefas trata de tempos e recursos. Uma precondição de bateria ausente pode fazer um plano válido no modelo falhar fisicamente. O monitoramento da execução verifica essa diferença. O planejamento automatizado chegou a sistemas reais, incluindo o Remote Agent da NASA na Deep Space 1 em 1999.