Lógica para Computação - Lógica de Predicados: Substituição de variáveis por termos, sentenças, satisfabilidade, prenex, - aula14

Prévia do material em texto

IF673 – Engenharia da Computação
Cin/UFPE – Anjolina Grisi de Oliveira
Lógica para Computação
2
Retomando o problema SAT
 Dado um conjunto C de sentenças da lógica de primeira ordem. Pergunta-se: C é satisfatível?
C tem um modelo?
De acordo com o que já estudamos, sabemos que se C for um conjunto de sentenças atômicas, a resposta é SIM. Sabemos como construir pelo menos um modelo, que é o modelo canônico. 
Resta saber o que fazer quando C contem fórmulas não atômicas.
3
Substituição de variáveis por termos
 Queremos definir precisamente o resultado da substituição das ocorrências de uma variável x numa FBF  por um termo t (em símbolos [t/x].
Se  é atômica temos [t/x]. É a fórmula resultante da remoção de todas as ocorrências de x e a colocação do termo t nos seus lugares.
Se  é da forma : ()[t/x]=([t/x])
Se  é da forma (): 
	()[t/x] = ([t/x]  [t/x]);
4. Se  é da forma (): 
	()[t/x] = ([t/x]  [t/x]);
5. Se  é da forma (): 
	()[t/x] = ([t/x]  [t/x]);
4
Substituição de variáveis por termos
Se  é atômica temos [t/x]. 
Se  é da forma : ()[t/x]=([t/x])
Se  é da forma (): 
	()[t/x] = ([t/x]  [t/x]);
4. Se  é da forma (): 
	()[t/x] = ([t/x]  [t/x]);
5. Se  é da forma (): 
	()[t/x] = ([t/x]  [t/x]);
Se  é da forma xi, (xi)[t/x]=
 - xi , se xi=x
	 - xi([t/x]), se xi  x 
7. Se  é da forma xi, (xi)[t/x]=
 - xi , se xi=x
	 - xi([t/x]), se xi  x 
5
Exemplos: substituição
 1) (x)(y)(P(x,y)  R(y))[a/x]
 2) (x)(y)(P(x,y) R(z))[f(a)/z]
 3) (x)(y)(P(x,y) R(z))[y/z]
 Atenção: Essa última substituição não pode ser realizada, pois muda o significado da fórmula. Antes z ocorria livre e agora seria substituída por uma variável ligada. Vejamos outro exemplo.
 4) (x)P(x,y)[x/y] 
Nesse exemplo, a substituição também não pode ser aplicada.
6
Exemplos: substituição
 5) (x)(P(x)  R(y))[f(x)/y]
 6) (x)(P(x) R(z))[f(z)/z]
 Atenção: Essa última substituição também não pode ser realizada. A variável que está sendo substituída não pode ocorrer no termo.
Nesse exemplo, a substituição também não pode ser aplicada.
7
Substituição de variáveis por termos
Podemos aplicar substituição também a termos somente. Usamos a mesma notação: s[t/x], para indicar a substituição da variável x pelo termo t no termo s.
Exemplos:
f(x)[a/x]
g(g(x,y),g(f(z),x))[a/x,b/y,f(c)/z]
h(x,y)[a/x,f(y)/y]
Essa última substituição não pode ser aplicada.
8
Valor-verdade de uma sentença
Seja L uma assinatura, A uma L-estrutura, e .A uma interpretação dos símbolos de L na L-estrutura. O valor-verdade de uma sentença  de L é definida indutivamente da seguinte forma:
 
Se  é atômica:
é da forma R(t1,...,tn): 
	A é verdade sse (t1A, ..., tnA)  RA;
2. é da forma t1=t2:
	 A é verdade sse (t1A = t2A).
Se  é da forma : 
	A é verdade sse () A é V sse A é falsa . 
9
Valor-verdade de uma sentença
 3. Se  é da forma (): 
	 A é V sse () A é V sse A é V e A é V. 
4. Se  é da forma (): 
	 A é V sse () A é V sse A é V ou A é V. 
5. Se  é da forma (): 
	 A é V sse () A é V sse ()A é V ou A é V
	 sse A é falsa ou A é V.
Se  é da forma x:
 A é V sse (x) A é V sse ()A [a/x] é V para todo elemento a do domínio da estrutura A.
7. Se  é da forma x:
	 A é V sse (x) A é V sse ()A [a/x] é V para algum elemento a do domínio da estrutura A.
10
Valor-verdade de uma sentença
 Essa maneira de definir quando uma sentença é verdadeira numa estrutura é conhecida como a noção de verdade em um ``modelo de Tarski´´, em referência ao lógico Alfred Tarski, que foi pioneiro nessa definição.
	É conhecida também como a definição de verdade por meio de uma meta-linguagem.
11
Satisfabilidade de uma sentença
 
 Seja L uma assinatura, A uma L-estrutura e  uma sentença de L.
 Dizemos que A satisfaz  sob a interpretação i: LA, se A for verdadeira. 
 Nessa caso usamos a notação A | 
12
Satisfabilidade de uma sentença
 
 Seja  uma sentença da lógica de predicados numa assinatura L.
  é satisfatível se existe uma L-estrutura A e uma interpretação i: LA tal que A satisfaz  
  é refutável se existe uma L-estrutura A e uma interpretação i: LA tal que A não satisfaz  
  é tautologia (válida) se para toda L-estrutura A e toda interpretação i: LA A satisfaz . 
  é insatisfatível se para toda L-estrutura A e toda interpretação i: LA , A não satisfaz  
 Nessa caso usamos a notação A 
13
Conjunto de Sentenças
 
 Suponha que  seja um conjunto de sentenças da assinatura L.
 é satisfatível se existe uma L-estrutura A e uma interpretação i: LA tal que A satisfaz cada uma das sentenças de . 
  é consequência lógica de  se para toda L-estrutura A e toda interpretação i: LA , se A satisfaz  então A satisfaz  
 
14
Equivalência Lógica
 
 
 é logicamente equivalente a  se para toda L-estrutura A e toda interpretação i: LA, A satisfaz  se e somente se A satisfaz .
15
Valor-verdade de uma fórmula
 Para calcular o valor-verdade de uma fórmula, precisamos antes aplicar uma substituição apropriada de variáveis livres da fórmula por termos fechados da linguagem L.
16
Satisfabilidade de uma fórmula
 
 Seja (x1,...,xn) uma fórmula da lógica de predicados numa assinatura L, na qual aparecem ocorrências livres das variáveis x1,...,xn.
  é satisfatível se existe uma L-estrutura A, uma interpretação i: LA e termos a1,...,an tais que A satisfaz [a1/x1, …an/xn]. 
  é refutável se existe uma L-estrutura A e uma interpretação i: LA e termos a1,...,an tais que A não satisfaz [a1/x1, …an/xn]. 
17
Satisfabilidade de uma fórmula
  é válida se para toda L-estrutura A, toda interpretação i: LA e toda n-upla a1,...,an de termos de L, A satisfaz [a1/x1, …an/xn]. 
  é insatisfatível se para toda L-estrutura A, toda interpretação i: LA e toda n-upla a1,...,an de termos de L, A não satisfaz [a1/x1, …an/xn]. 
18
Resolução para lógica de predicados
 Temos os mesmos conceitos: literal, cláusula e forma normal conjuntiva.
 Novo: eliminação dos quantificadores: o conceito de fórmula na forma padrão de Skolem.
 Novo: conceito de fórmula normal prenex
 Novo: o conceito de unificação.
19
Forma Normal Prenex
  Definição : Uma fórmula  na lógica de primeira ordem está na forma normal prenex se e somente se a fórmula F está na forma:
		(Q1x1)...(Qnxn)(M)
onde cada (Qixi), i = 1,...,n, ou é (xi) ou (xi), e M é uma fórmula sem quantificadores.
(Q1x1)...(Qnxn) é chamado de prefixo e M de matriz da fórmula .
20
Exemplos
 1) (x)(P(x,y)  R(y))
 2) (x)(y)(z)(P(x,y) R(z))
21
 Fórmula normal prenex
Teorema 
Suponha que  é uma fórmula da lógica de predicados numa assinatura L. Então existe uma fórmula  da lógica de predicados na mesma assinatura L, de forma que:
 está na forma normal prenex;
 é logicamente equivalente a .
22
 Fórmula normal prenex
Para transformar uma fórmula para a forma normal prenex, nós usamos as equivalências lógicas que já estudamos na lógica proposicional e algumas leis novas. Antes, porém vamos introduzir a seguinte notação:
Seja F uma fórmula que contem uma variável x. Para enfatizar essa informação, nós vamos representar F como F[x];
Usamos a letra Q para denotar um quantificador.
Nas leis que vamos definir, a fórmula G não contem a variável x;.
23
 Fórmula normal prenex
(Qx)F[x]  G = (Qx)(F[x]  G)
(Qx)F[x]  G = (Qx)(F[x]  G)
((x)F[x]) = (x)(F[x])
((x)F[x]) = (x)(F[x])
24
 Fórmula normal prenex
5. (x)F[x] (x)H[x] = (x)(F[x]  H[x])
6. (x)F[x]  (x)H[x] = (x)(F[x]  H[x])
 (x)F[x] (x)H[x]  (x)(F[x]  H[x])
 (x)F[x]  (x)H[x]  (x)(F[x]  H[x])
O que fazer nesses casos?
7. (x)F[x]  (x)H[x] = (x)F[x] (z)H[z] = (x)(z)(F[x]  H[z]) (renomear variáveis ligadas)
(x)F[x]  (x)H[x] = (x)(F[x]  (z)H[z] = (x)(z)(F[x]  H[z]) 
25
 Fórmula normal prenex
Eliminar os conectivos  e .
Repetidamente usar:
	- (G)=G
	- as leis de De Morgan
	- e as leis ((x)F[x]) = (x)(F[x])
 ((x)F[x]) = (x)(F[x])
 para colocar a negação imediatamente antes dos átomos.
3. Usar as leis novas para deixar a fórmula na forma normal prenex.
26
 Fórmula normal prenex: exemplos
xP(x)  xQ(x).
xy(z(P(x,z)  P(y,z))  uQ(x,y,u)).