Aula Prática 4 – Lógica proposicional e inferência

Matéria das aulas T8 (agentes lógicos: lógica proposicional, sintaxe e semântica) e T9 (inferência proposicional: resolução, cláusulas de Horn, DPLL, WALKSAT, agentes). Os exercícios são para trabalho autónomo, individualmente ou em grupos de dois. Os exercícios que ficarem por resolver na aula devem ser resolvidos em casa. Partes desta matéria apenas recapitulam matéria anteriormente dada na Unidade Curricular de Lógica Computacional, seguindo as convenções do AIMA, 4.ª edição.

Convenções

Toda a terminologia é a do AIMA, 4.ª edição (capítulo 7, com a mesma numeração nas edições americana e global) e a dos slides T8 e T9.

• Nas tabelas de verdade, os símbolos vêm por ordem alfabética e as linhas pela ordem V-antes-de-F do primeiro símbolo, depois do segundo, etc. (como na fig. 7.9). Quando se pede «o(s) modelo(s)», pede-se a atribuição a todos os símbolos.
• Uma cláusula é uma disjunção de literais; escreve-se cada cláusula uma só vez, sem literais repetidos, e descartam-se as tautologias (cláusulas com ℓ e ¬ℓ). A cláusula vazia escreve-se □.
• Na resolução, cada passo resolve um par de literais complementares de duas cláusulas. Numa prova por resolução, numere as cláusulas e indique, em cada passo, as duas cláusulas-mãe e o símbolo sobre o qual se resolve.
• O DPLL é o da fig. 7.17, com a ordem de verificação do próprio algoritmo: primeiro a terminação antecipada; depois o símbolo puro (se houver vários, o primeiro por ordem alfabética); depois a cláusula unitária (se houver várias, a primeira pela ordem em que as cláusulas estão escritas); e por fim a divisão (split) (o primeiro símbolo por atribuir, por ordem alfabética, com verdadeiro antes de falso). Nas provas, o traço apresenta-se como uma tabela com uma linha por passo: n.º, tipo (puro / unitária / divisão / retrocesso), variável, valor.
• No WALKSAT (fig. 7.18), os empates são resolvidos pela ordem alfabética.

Exercício 1 – Da história à inferência

Três amigos — a Ana, o Bruno e a Carla — vão jantar fora. Sobre quem pede sopa sabe-se o seguinte: pelo menos um dos três pede sopa; se a Ana pede sopa, o Bruno também pede; e a Carla só pede sopa se o Bruno não pedir.

(a) Escolha símbolos proposicionais e escreva a base de conhecimento KB (três frases).

(b) Quantos modelos há para estes símbolos? Construa a tabela de verdade e assinale os modelos de KB. Quantos são?

(c) Usando a tabela, decida se cada uma das frases seguintes é consequência lógica de KB: α₁ = «o Bruno pede sopa», α₂ = «o Bruno ou a Carla pedem sopa», α₃ = «a Ana e a Carla não pedem ambas sopa». Para as que não são, apresente um contra-modelo. O que faria TT-ENTAILS? em cada caso?

(d) Converta KB para FNC e classifique cada cláusula (definida, de Horn, objectivo, nenhuma). A KB toda é de Horn?

(e) Prove por resolução (refutação) que α₂ é consequência lógica de KB: acrescente as cláusulas de ¬α₂ e derive □.

(f) Repita a prova de α₂ com o DPLL sobre as cláusulas de KB ∧ ¬α₂, apresentando o traço na forma das provas (n.º, tipo, variável, valor). Que relação há entre o DPLL devolver false e KB ⊨ α₂?

Exercício 2 – Sintaxe e semântica

(a) Classifique cada frase como válida, satisfazível mas não válida ou insatisfazível, justificando com uma tabela de verdade ou com um argumento curto.

1. (P ⇒ Q) ∨ (Q ⇒ P)
2. (P ⇒ Q) ∧ (P ⇒ ¬Q)
3. (P ∧ (P ⇒ Q)) ⇒ Q
4. (P ⇔ Q) ∧ (P ⇔ ¬Q)
5. ((P ⇒ Q) ⇒ P) ⇒ P
6. (P ∨ Q) ⇒ (P ∧ Q)

(b) Para cada afirmação, diga se é verdadeira ou falsa e justifique (um contra-modelo chega para as falsas).

1. (A ∧ B) ⊨ (A ⇔ B)
2. (A ⇔ B) ⊨ (A ∨ B)
3. (A ⇔ B) ⊨ (¬A ∨ B)
4. (A ∨ B) ∧ (¬C ∨ ¬D ∨ E) ⊨ (A ∨ B)
5. (A ∨ B) ∧ (¬C ∨ ¬D ∨ E) ⊨ (A ∨ B) ∧ (¬D ∨ E)
6. (A ∨ B) ∧ ¬(A ⇒ B) ⊨ A
7. C ∨ (¬A ∧ ¬B) ≡ (A ⇒ C) ∧ (B ⇒ C)
8. (A ∧ B) ⇒ C ≡ (A ⇒ C) ∨ (B ⇒ C)

(c) Enuncie o teorema da dedução e use-o para reescrever a afirmação (b)(i) como uma frase válida e como uma frase insatisfazível. Porque é que a segunda forma é a base dos métodos de prova por refutação?

(d) Com n símbolos proposicionais, quantos modelos tem: uma frase válida? um literal? uma cláusula com k literais (de símbolos distintos)? uma conjunção de k literais de símbolos distintos? uma frase insatisfazível? Confirme a resposta da cláusula com n = 3, k = 2.

(e) O «ou» e o «implica» da lógica não são exactamente os da linguagem natural. Diga se cada frase é verdadeira ou falsa, como frase de lógica proposicional, num modelo em que os factos que conhece do mundo são verdadeiros: «5 é ímpar ⇒ Tóquio é a capital do Japão»; «5 é par ⇒ Lisboa é a capital de Espanha»; «2 é par ∨ 2 é primo». Que tipo de «ou» é o ∨?

Exercício 3 – O mundo do wumpus: duas brisas

O agente começa em [1,1], onde não sente brisa nem cheiro. Avança para [2,1] e sente brisa; volta a [1,1], sobe a [1,2] e sente brisa outra vez. Não há cheiro em nenhuma das três casas. A figura mostra o que o agente sabe, com a notação do livro (V = visitada, B = brisa, OK = casa segura, P? = poço possível).

(a) Escreva a KB relevante para os poços: a frase que diz que não há poço em [1,1], os três axiomas da brisa (um bicondicional para cada casa visitada — as casas da coluna 1 e da linha 1 têm menos vizinhas) e as três percepções.

(b) Converta o axioma da brisa de [2,1] para FNC. Quantas cláusulas dá um axioma de uma casa com k vizinhas? Para o tabuleiro 4 × 4 inteiro (16 axiomas da brisa), quantas cláusulas são?

(c) Que casas são OK (sem poço, de certeza)? Mostre, exibindo dois modelos de KB, que KB ⊭ P₂,₂ e KB ⊭ ¬P₂,₂: o agente não sabe se há poço em [2,2].

(d) Prove por resolução que KB ⊨ P₂,₂ ∨ P₃,₁. Depois, sem nova prova, justifique que KB ⊨ P₂,₂ ∨ (P₃,₁ ∧ P₁,₃) — que equivalência da fig. 7.11 usa?

(e) Fixados os valores que KB determina, os símbolos que ficam livres são P₂,₂, P₃,₁ e P₁,₃. Quantos modelos tem KB sobre estes três símbolos? Em quantos deles há poço em [2,2]? E em [3,1]? Se o agente fosse obrigado a avançar para uma casa não OK, qual escolheria com base nesta contagem? O que diz a lógica, e o que não diz, sobre o risco? (Os slides do T8 dão 0,86 e 0,31 para este caso — de onde virá a diferença? É matéria do T15.)

(f) Se a KB tivesse os 16 axiomas da brisa e todos os símbolos P e B do tabuleiro, quantos símbolos teria, e quantos modelos enumeraria TT-ENTAILS? para responder a (c)? O que é que a sua resposta a (e) faz de diferente?

Exercício 4 – Forma normal conjuntiva e resolução

(a) Converta para FNC, indicando os quatro passos:

1. (A ⇒ B) ⇒ C
2. ¬(A ∧ (B ⇒ C))
3. (A ∨ B) ⇔ C
4. (A ⇔ B) ⇔ C

Na alínea iv, que cláusulas descartou, e porquê?

(b) Resolva os pares de cláusulas seguintes e comente o resultado.

1. (A ∨ B ∨ ¬C) e (¬A ∨ ¬B ∨ D) — quantos resolventes há? São úteis?
2. (A ∨ B) e (A ∨ ¬B) — o que é a factorização?
3. (P₁,₁ ∨ P₃,₁) e (¬P₁,₁ ∨ ¬P₂,₂) — o exemplo dos slides.

(c) Considere a KB = { A ∨ B, A ⇒ C, B ⇒ (C ∨ D), D ⇒ A }.

1. Escreva as cláusulas de KB.
2. Prove por resolução que KB ⊨ C. Numere as cláusulas e indique as mães de cada resolvente.
3. KB ⊨ A? Responda com um modelo. Como é que o PL-RESOLUTION chegaria à mesma conclusão — e porque é que, em lógica proposicional, ele termina sempre?

(d) O teorema da resolução básica diz que a resolução é completa por refutação. O que é que isso garante, e o que é que não garante? Dê um exemplo de uma frase α com KB ⊨ α que não se obtém de KB só por aplicação da regra da resolução (sem refutação).

Exercício 5 – Cláusulas de Horn e encadeamentos

Considere a base de conhecimento, com os factos A e B:

(a) Escreva cada frase como cláusula (disjunção de literais) e verifique que todas são cláusulas definidas. Se a KB tivesse também a frase C ⇒ (D ∨ E), que tipo de cláusula seria, e porque é que os dois encadeamentos deixavam de se poder aplicar?

(b) Desenhe o grafo E-OU da KB (como na fig. 7.16).

(c) Aplique o encadeamento para a frente (PL-FC-ENTAILS?) para a pergunta G. Em cada passo indique o símbolo que sai da agenda (queue), os contadores das regras e a agenda. Em que passo o algoritmo responde?

(d) Continue o encadeamento até a agenda esvaziar (como se a pergunta fosse H). Que símbolos ficam inferidos? O que acontece quando G é retirado da agenda pela segunda vez? Que relação há entre o conjunto final de símbolos inferidos e os modelos de KB?

(e) Aplique o encadeamento para trás à pergunta G, com as convenções. Em que ponto a detecção de ciclos é necessária? Compare o trabalho feito com o de (c): que factos e regras o encadeamento para trás nem chegou a tocar?

(f) H é consequência lógica de KB? Justifique com um modelo. Diga qual é a complexidade dos dois encadeamentos e por que razão a inferência em cláusulas de Horn é tão mais barata do que no caso geral.

Exercício 6 – DPLL e WALKSAT

(a) Verifique, usando o algoritmo DPLL, se o conjunto de cláusulas seguinte é satisfazível. Apresente o traço na forma das provas (n.º, tipo, variável, valor) e, se for satisfazível, o modelo.

{ (A ∨ B), (¬A ∨ E), (¬A ∨ ¬D ∨ ¬E), (¬B ∨ C), (¬B ∨ ¬C), (B ∨ ¬C), (C ∨ ¬D ∨ ¬E) }

(b) Usando apenas o traço do DPLL de (a), C é consequência lógica do conjunto de cláusulas de (a)?

(c) Verifique, usando o DPLL, se D é consequência lógica do conjunto de frases

{ A ⇒ ¬C, ¬B ⇒ E, B ⇔ ¬A, B ⇔ (D ∨ A) }

Comece por escrever as cláusulas de KB ∧ ¬D.

(d) Quantos modelos enumeraria TT-ENTAILS? em (a)? Quantas atribuições (linhas de divisão / retrocesso) fez o DPLL? Que três melhorias explicam a diferença?

(e) Repita (a) com falso antes de verdadeiro na divisão. E com a cláusula unitária verificada antes do símbolo puro? Compare o número de passos e comente a afirmação «a ordem das heurísticas e das divisões não influencia o tempo de execução do DPLL».

(f) Aplique o WALKSAT ao conjunto de (a), com p = 0,5, a partir do modelo em que todos os símbolos são falsos. Em cada passo há uma só cláusula falsa; a moeda deu, por esta ordem, passeio, ganho, passeio, ganho; nos passeios o símbolo sorteado foi B e depois A. Mostre o modelo em cada passo e o número de cláusulas satisfeitas por cada inversão possível nos passos de ganho. O que teria acontecido no segundo passo sem a regra de desempate? O que pode o WALKSAT concluir se o conjunto for insatisfazível?

Exercício 7 – Agentes baseados em lógica proposicional

(a) Classifique cada símbolo como fluente, percepção, acção ou atemporal: L^t₁,₁, HaveArrow^t, P₃,₁, Breezy₂,₁, Breeze^t, Stench^t, WumpusAlive^t, FacingEast^t, Forward^t, OK^t₂,₂, W₁,₃.

(b) Escreva o axioma de efeito da acção Forward para um agente em [1,1] virado a este, no instante t. O que fica por dizer sobre L^{t+1}₁,₁ e sobre HaveArrow^{t+1}? Como se chama este problema, e quantos axiomas de enquadramento por instante seriam precisos num mundo com m acções e n fluentes?

(c) Escreva os axiomas de estado sucessor de

1. HaveArrow (o dos slides, (7.2)),
2. WumpusAlive (o agente ouve Scream^{t+1} quando o wumpus morre),
3. FacingEast (as acções TurnLeft e TurnRight rodam 90°),
4. L₂,₁ (adapte o (7.3), que é o de L₁,₁; a casa [2,1] tem três vizinhas).

Quantos axiomas de estado sucessor por instante tem o mundo 4 × 4 (16 casas, 4 orientações, HaveArrow, WumpusAlive, HaveGold)?

(d) Escreva o axioma que liga a percepção de brisa à casa: «se o agente está em [x, y] no instante t, sente brisa sse a casa é ventosa». Porque é que Breezy_{x,y} é atemporal e Breeze^t não? Escreva também a definição de OK^t_{x,y}.

(e) O problema da qualificação: dê um exemplo de uma condição que o axioma de (b) ignora. Porque é que não se resolve «acrescentando mais uma premissa»?

(f) No SATPLAN, a primeira versão da KB admitia um plano em que o agente estava em duas casas ao mesmo tempo. Escreva o axioma de precondição de Shoot e o axioma de exclusão entre Forward e Shoot. Com m acções, quantos axiomas de exclusão por instante são precisos, e qual é a alternativa com apenas um axioma?

Exercício 8 – Verdadeiro ou falso

Indique se cada afirmação é verdadeira ou falsa e justifique numa frase.

1. Toda a cláusula definida é uma cláusula de Horn.
2. Existe um conjunto de cláusulas de Horn do qual a atribuição «todos os símbolos falsos» não é modelo.
3. Se KB ⊨ α e KB ⊨ ¬α, então KB é insatisfazível.
4. Se α é válida, então KB ⊨ α para qualquer KB.
5. Se KB é insatisfazível, então KB ⊨ α para qualquer α.
6. Acrescentar frases a KB pode fazer com que uma frase que era consequência lógica deixe de o ser.
7. Se KB ⊨ α, então α pode ser derivada de KB por aplicações sucessivas da regra da resolução.
8. O DPLL sem a regra do símbolo puro deixa de ser completo.
9. O DPLL é mais eficiente do que a enumeração de tabelas de verdade, mas perde completude.
10. A ordem pela qual o DPLL aplica as heurísticas e faz as divisões não influencia, em geral, o tempo de execução.
11. O WALKSAT pode provar que um conjunto de cláusulas é insatisfazível.
12. O encadeamento para a frente é sólido e completo para KBs de cláusulas definidas, e corre em tempo linear.
13. Decidir se uma frase proposicional é satisfazível é NP-completo; decidir se é válida é coNP-completo.
14. Para frases 3-FNC aleatórias com n símbolos e m cláusulas, as instâncias mais difíceis aparecem perto de m/n ≈ 4,3.
15. Se a conversão de uma frase para FNC produz a cláusula vazia, a frase é válida.
16. Um axioma de estado sucessor por fluente substitui todos os axiomas de efeito e de enquadramento desse fluente.