p2-2012.2 - Prova e Gabarito

Prévia do material em texto

UFPE / CIn/ Engenharia da Computação 
Lógica para Computação / Segunda Avaliação / 2012.2 - 16/04/2012 GABARITO 
1. (3,0) Considere as seguintes fórmulas na lógica de predicados que descrevem as 
propriedades simétrica, transitiva e total de uma relação binária R: 
 1: xy (R(x,y)  R(y,x)) 
 2: xyz ( (R(x,y)  R(y,z)) R(x,z) ) 
 3: xy (R(x,y)) 
 Use o princípio da resolução para provar que se uma relação binária é simétrica, transitiva e 
total então ela também é reflexiva. Ou seja, {1, 2, 3}├ x (R(x,x)) 
Cláusulas={ c1: R(x,y)  R(y,x)), c2:R(x,y)  R(y,z) R(x,z), c3:R(x,f(x)) c4:R(a,a)} 
Nesse caso, apesar de termos as mesmas variáveis, não haverá problemas e portanto não precisa 
renomeá-las. 
c1 e c3 [f(x)/y]: R(f(x),x) (c5) 
c5 e c2[f(x)y, x/z]: :R(x,f(x))  R(x,x) (c6) 
c6 e c3: R(x,x) (c7) 
c7 e c4[a/x]:  
 
2. (2,5) Use o algoritmo de Herbrand para determinar se os seguintes conjuntos de termos 
são unificáveis. Mostre os passos do algoritmo. Se a unificação for possível mostre o 
unificador (ou seja, as substituições necessárias), caso contrário, explique o motivo. 
 
a) {f(x,g(y)), f(g(u),h(z))} 
Resp.: { f(x,g(y))= f(g(u),h(z)) } 
Decomposição de termos: 
{ x= g(u), g(y) = h(z) } 
Impossível fazer a unificação entre os termos g(y) e h(z). 
 
b) {f(x,g(x),x), f(g(u),g(g(z)),z)} 
Resp.: {f(x,g(x),x)= f(g(u),g(g(z)),z)} 
Decomposição de termos 
{x=g(u), g(x)= g(g(z)), x=z} 
Eliminação de variáveis:[g(u)/x] 
{x=g(u), g(g(u))= g(g(z)), g(u) = z} 
Decomposição de termos: 
{x=g(u), g(u)=g(z), g(u) = z} 
Decomposição de termos: 
{x=g(u), u=z, g(u)=z} 
Eliminação de variáveis [g(u)/z] 
{x=g(z), u=g(u), g(z)=z} 
Impossível unificar os termos pois u ocorre em g(u). 
 
c) {f(x,f(x,y)), f(g(y), f(g(a),z))} 
Resp.: {f(x,f(x,y))= f(g(y), f(g(a),z))} 
Decomposição de termos 
{x=g(y), f(x,y) = f(g(a),z)} 
Decomposição de termos: 
{ x=g(y), x=g(a), y=z } 
Eliminação de variáveis:[g(a)/x] 
{g(a)=g(y), x=g(a), y=z} 
Decomposição de termos 
{y=a, x=g(a), y=z} 
Eliminação de variáveis: [a/y] 
{y=a, x=g(a), z=a} 
Sistema resolvido e essa substituição é o unificador. 
 
 
3. (2,5) Dada a estrutura A: (i) domínio: o conjunto dos números inteiros; (ii) elementos 
destacados: o número 0; (iii) relações: Maior-Que (binária), Impar (unária), Primo (unária); 
(iv) funções: sucessor (unária), soma (binária), antecessor(unária) 
 
a) Defina uma assinatura L para A. 
Destaques: a 
Um símbolo de relação binária: M 
Dois símbolos de relação unária: I e P 
Dois símbolos de função unária: ant e suc 
Um símbolo de função binária: s 
 
b) Defina indutivamente o conjunto dos termos de L 
 
 Toda variável é um termo 
 a é um termo 
 Se t é um termo então ant(t) e suc(t) também são termos 
 Se t e u são termos então s(t,u) também são termos 
 Nada mais é um termo de L. 
 
c) Defina o diagrama positivo de A 
 
M(suc(a),a), M(a,ant(a)), P(suc(suc(a))), P(s(suc(a),suc(a))), I(suc(a)), I(suc(suc(suc(a)))), 
a=suc(ant(a)), s(suc(a),a) = suc(a), ant(suc(a) = a, s(a,a) = a ..... 
 
d) Dê uma fórmula que contenha pelo menos uma variável ligada, pelo menos um dos 
símbolos de função na qual A seja modelo e outra na qual A seja contra-modelo. (As 
duas fórmulas também devem incluir pelo menos dois dos predicados). 
 
Modelo: z(P(z)  (z=suc(suc(a)))  I(z)) 
Contra-modelo: x(M(x,suc(x))  zw (I(z)  I(w)  I(s(z,w))) 
 
4. (2,0) Explique qual a importância do teorema de Herbrand. Fale também quais foram as 
tentativas de implementá-lo. Diga se alguma delas foi bem sucedida e qual o motivo. 
O teorema de Herbrand é de fundamental importância para os provadores automáticos de 
teoremas. Ele diz que se um conjunto de cláusulas é insatisfatível, o conjunto de instâncias básicas 
dessas cláusulas é insatisfatível também. Para encontrar o conjunto de instâncias básicas de 
cláusulas, substituímos as variáveis por termos de um domínio específico, chamado de universo de 
Herbrand. Como existe uma quantidade infinita de domínios, a importância desse teorema se dá 
pela garantia que se tem de que basta construir a prova para o universo de Herbrand. 
Existiram várias tentativas para implementar o teorema. Dentre elas, destacam-se os trabalhos de 
Davis e Putnam, Gilmore e Robinson. Os trabalhos de Gilmore e Davis e Putnam foram 
importantes, mas se mostraram ineficientes devido a geração dos diversos conjuntos de instâncias 
básicas de cláusulas. No entanto, ao propor o método da resolução com a incorporação do 
algoritmo de unificação, Robinson propôs um algoritmo mais eficiente, sem a necessidade da 
geração dos conjuntos de instâncias básicas de cláusulas. Essas instâncias são computadas 
diretamente com o algoritmo de unificação. 
 
EXTRA (1,0) (SOMENTE PARA QUEM FALTOU UMA MINI-PROVA) 
 
Use resolução para provar: 
 
 {x(P(x,a)  Q(x)), y(P(f(y),a)  Q(y))} |= x(Q(x)  Q(f(x)))