Aulas_-_Lógica_de_Predicados

Prévia do material em texto

________________________________________________________________________________________ 
 
Prof. Sérgio Gorender Lógica 
Lógica de Predicados de Primeira Ordem 
 Trata com objetos e suas propriedades. 
todo o a é um b 
A é um a 
A é um b 
 Permite expressar afirmativas sobre elementos das 
estruturas. 
 Sistema formal apropriado para a definição de 
teorias do universo de discurso da matemática. 
• Sistema formal – composto de uma linguagem 
formal e de uma abstração adequada para os 
princípios usados para decidir quando uma 
assertiva é conseqüência lógica de outras. 
• Teoria – conjunto de assertivas (proposições, 
lemas, teoremas, etc.) acerca de um universo de 
discurso. 
________________________________________________________________________________________ 
 
Prof. Sérgio Gorender Lógica 
• Formalização de uma teoria – 
 Escolher uma nova linguagem simbólica ou 
formal para exprimir a teoria, em substituição a 
uma linguagem natural. 
 Organizar as assertivas da teoria dedutivamente, 
escolhendo algumas assertivas como axiomas 
ou postulados a partir das quais as demais 
podem ser gradativamente obtidas. 
 Exprimi-se também as propriedades dos termos 
do universo de discurso através de novos 
axiomas até que o significado destes termos não 
precise mais ser usado nas deduções. 
 Explicita-se o significado dos termos ordinários 
(fora do universo de discurso) e os princípios 
usados para decidir quando uma assertiva é 
conseqüência lógica de outras. 
________________________________________________________________________________________ 
 
Prof. Sérgio Gorender Lógica 
Originou-se no “Begriffsschrift” publicado por 
Gotlob Frege em 1879. 
Outros resultado importantes para a lógica de 
primeira ordem – 
• Gödel – provou a existência de um sistema 
axiomático consistente e completo para a Lógica 
de Primeira ordem, em sua tese de doutorado – 6 
de fevereiro de 1930. 
• Herbrand – obteve uma solução para o problema 
da caracterização dos princípios lógicos de 
primeira ordem que se tornou fundamental para a 
mecanização da lógica – 11 de junho de 1930. 
• Skolem – solução alternativa para o problema da 
caracterização, de certa forma semelhante aos 
resultados de Herbrand. 
• Church e Turing – indecidibilidade do problema 
da validade (1936). Obtiveram seus resultados de 
forma independente. 
• Problema da validade – determinar se existe 
ou não um algoritmo que recebe como 
entrada qualquer fórmula de primeira ordem e 
produz como saída SIM, se a fórmula é 
sempre válida, e NÃO em caso contrário. 
________________________________________________________________________________________ 
 
Prof. Sérgio Gorender Lógica 
 Sintaxe das linguagens de primeira ordem – 
• Um alfabeto de primeira ordem contém – 
conectivos lógicos, parênteses, variáveis (para 
denotar indivíduos arbitrários do domínio de 
discurso), constantes (para denotar indivíduos 
específicos), símbolos para denotar funções ou 
relações (predicados) e quantificadores. 
• Termos são seqüências de símbolos que denotarão 
indivíduos do domínio do discurso. 
• Fórmulas simples são seqüências de símbolos que 
representam relacionamentos entre indivíduos e 
que receberão valores verdade V ou F. 
________________________________________________________________________________________ 
 
Prof. Sérgio Gorender Lógica 
• Alfabeto de primeira ordem A – 
 Símbolos lógicos – 
Pontuação: (, ) 
Conectivos: ¬, ∧, ∨, →, ≡ 
Quantificadores: ∀ (quantificador universal – 
para todo) 
∃ (quantificador existencial – 
existe) 
Variáveis: um conjunto de símbolos distinto 
dos demais- x, y, z, w, .... 
Símbolo de igualdade: = 
________________________________________________________________________________________ 
 
Prof. Sérgio Gorender Lógica 
 Símbolos não-lógicos- 
♦ Um conjunto, possivelmente vazio, de 
constantes distintas dos demais símbolos. 
 a, b, c, d, ... 
♦ Um conjunto, possivelmente vazio, de 
símbolos funcionais n-ários distintos dos 
demais símbolos, sendo n>0. 
 f, g, h, i, ... 
♦ Um conjunto, possivelmente vazio, de 
símbolos predicados n-ários distintos dos 
demais símbolos, sendo n>0. 
 P, Q, R, S, T, ... 
________________________________________________________________________________________ 
 
Prof. Sérgio Gorender Lógica 
• Conjunto dos termos de primeira ordem sobre um 
alfabeto de primeira ordem A: 
 Toda variável em A é um termo sobre A. 
 Toda constante em A é um termo sobre A. 
 Se t1,...,tn são termos sobre A e f é um símbolo 
funcional n-ário de A, então f(t1,...,tn) também é 
um termo sobre A. 
________________________________________________________________________________________ 
 
Prof. Sérgio Gorender Lógica 
• Conjunto de fórmulas sobre um alfabeto de 
primeira ordem A: 
 Se t1,...,tn são termos sobre A e P é um símbolo 
predicativo n-ário de A, então P(t1,...,tn) é uma 
fórmula sobre A, chamada de fórmula atômica. 
 Se t1 e t2 são termos sobre A e “=” é um símbolo 
de A, então (t1 = t2) é uma fórmula sobre A, 
também chamada de fórmula atômica. 
 Se P e Q são fórmulas sobre A, então (¬P), 
(P ∧ Q), (P ∨ Q), (P → Q) e (P ≡ Q) também 
são fórmulas sobre A. 
 Se P é uma fórmula sobre A e x é uma variável 
de A, então ∀x(P) e ∃x(P) também são 
fórmulas sobre A. 
________________________________________________________________________________________ 
 
Prof. Sérgio Gorender Lógica 
• Linguagem de primeira ordem L(A), sobre um 
alfabeto de primeira ordem A – conjunto de 
termos e fórmulas de primeira ordem sobre A. 
• Escopo de um quantificador – subfórmula Q da 
fórmula ∀x (Q) (válido para ∃). 
• Ocorrência ligada de uma variável x em uma 
fórmula P – x ocorre em uma subfórmula de P na 
forma ∀x (Q) (válido para ∃). 
________________________________________________________________________________________ 
 
Prof. Sérgio Gorender Lógica 
• Semântica das linguagens de primeira ordem – 
 Escolha de um mapeamento associando a cada 
símbolo não-lógico do alfabeto um elemento de 
um conjunto, uma função ou uma relação sobre 
este conjunto, dependendo do tipo do símbolo. 
 Considere – 
• A – um alfabeto de primeira ordem. 
• U – um conjunto não vazio. 
• I - função mapeando os símbolos de A sobre 
o universo U: 
 A cada constante c de A, I associa um elemento 
de U, denotado por I(c). 
 A cada símbolo funcional n-ário f de A, I 
associa uma função de Um em U, denotada por 
I(f). 
 A cada símbolo predicativo n-ário P de A, I 
associa uma relação sobre Um, denotada por 
I(P). 
 Função de avaliação para A sobre I – função v 
que associa a cada variável de A um elemento 
de U. 
 Função de avaliação para L(A) induzida por 
uma estrutura I e uma função de avaliação v 
para o alfabeto A é a função ν(v,I): L(A) → U 
∪ {F,V}. 
________________________________________________________________________________________ 
 
Prof. Sérgio Gorender Lógica 
 Avaliação dos termos – 
ν[v,I](x) = v(x), para cada variável x de A. 
ν[v,I](c) = I(c), para cada constante c de A. 
ν[v,I](f(t1,...,tn)) = I(f)(ν[v,I](t1),...,ν[v,I](tn)) 
 Avaliação das fórmulas – 
ν[v,I](t1 = t2) = V, se ν[v,I](t1) = ν[v,I](t2) 
F, em caso contrário 
ν[v,I](P(t1,...,tn)) = V, se d1,...,dn) ∈ I(P) 
F, em caso contrário 
onde di = ν[v,I](ti), para i = 1,...,n 
ν[v,I](~p) = V, se ν[v,I](p) = F 
 F, se ν[v,I](P) = V 
ν[v,I](P∧Q) = V, se ν[v,I](P) = ν[v,I](Q) = V 
F, em caso contrário 
ν[v,I](P∨Q) = F, se ν[v,I](P) = ν[v,I](Q) = F 
V, em caso contrário 
ν[v,I](P→Q) = F, se ν[v,I](P) = V e ν[v,I](Q) = F 
V, em caso contrário 
ν[v,I](P≡Q) = V, se ν[v,I](P) =ν[v,I](Q) 
F, em caso contrário 
________________________________________________________________________________________ 
 
Prof. Sérgio Gorender Lógica 
ν[v,I](∀x(P)) = V, se ν[u,I](P) = V para toda função 
de avaliação u para A diferindo de 
v apenas no valor de x 
F, em caso contrário 
ν[v,I](∃x(P)) = V, se ν[u,I](P) = V para alguma 
função de avaliação u para A 
diferindo de v apenas no valor de 
x 
F, em caso contrário. 
 
 
________________________________________________________________________________________ 
 
Prof. Sérgio Gorender Lógica 
 Exercícios 
• Seja I uma interpretação sobre o domínio U dos números racionais 
(Q)*, diferentes de zero, tal que I[a]=1, I[b]=25, I[x]=13, 
I[y]=77,I[f]=÷, I[p]=<. 
)),,((),()
)),(),(()
),(),()
))),,((),(()
)),(,(),()
),()
),()
xbafPyxyPxg
yxPyxyPxf
yxPyxyPxe
bbafPyxPyxd
bafbPyxyPxc
yxxPb
yxyPxa
→∃∀
→∃∀
→∃∀
→∃∀
→∃∀
∃
∃∀
 
 
• Seja J uma interpretação sobre os números inteiros Z, tal que: J[a]=0, 
J[x]=-1, J[y]=0, J[P]=<, J[Q]=>, J[f]=fJ, onde fJ(d) = d + 1. Determine 
as interpretações das fórmulas a seguir. 
)),(),(()
)),(),(()
)),(),(()
))(,(),()
),()
))),((),(()
),()
yxQyxPxe
yxQyxPxd
yxQyxPxc
xfxPaxPd
yxxPyc
yyfPayPyb
xyyPa
∧∃
∨∃
∨∀
∧
∀∃
∨∀
∃
 
________________________________________________________________________________________ 
 
Prof. Sérgio Gorender Lógica 
 Propriedades semântica 
• Satisfazibilidade de fórmulas: 
 Uma fórmula H é satisfazível quando existe 
pelo menos uma interpretação I tal que I[H] = V 
• Fórmula válida: 
 Uma fórmula H não é válida (não é uma 
tautologia) se existe uma interpretação J tal que 
J[H] = F. 
 Duas fórmulas H e G são iguais em uma 
interpretação I se I[H] = V ↔ I[G] = V. 
 Uma fórmula G é uma tautologia se para toda 
interpretação J, temos que J[G] = V. 
________________________________________________________________________________________ 
 
Prof. Sérgio Gorender Lógica 
 Dedução Natural. 
• Apresentado em 1934 por Gentzen, como o 
cálculo NJ para a Lógica Intuicionística, e como o 
cálculo NK para a Lógica Clássica. 
• Composto de regras de introdução e eliminação 
para cada conectivo lógico, e para os 
quantificadores. 
• Princípio da inversão – a regra de introdução é o 
inverso da regra de eliminação. 
________________________________________________________________________________________ 
 
Prof. Sérgio Gorender Lógica 
• Regras de inferência: 
 Conjunção: 
 Disjunção: 
 Implicação: 
• A introdução da implicação é conhecida 
como regra de descarte, pois descarta uma 
suposição. Uma suposição descartada não 
poderá ser novamente utilizada na prova. 
• A regra de eliminação é o Modus Ponens. 
∧−
∧
I
BA
BA 
∧−
∧
1E
A
BA ∧−∧ 2E
B
BA
∨−
∨
1I
BA
A
∨−
∨
E
C
CCBA
BA
 
][ ][ ∨−
∨
2I
BA
B
→−
→
I
BA
B
A][
→−
→
E
B
ABA 
________________________________________________________________________________________ 
 
Prof. Sérgio Gorender Lógica 
 Negação: 
• A regra de introdução pode ser vista como um 
caso especial da introdução da implicação, 
visto que ¬A é uma abreviação de A→Λ. Λ 
significa a contradição, o falso. 
• A primeira regra de eliminação da negação 
representa e lei de contradição. A segunda 
expressa o fato de que se uma proposição 
falsa procede então qualquer proposição 
procede. 
¬−
¬
Λ
I
A
A][
¬−
Λ
¬
1
 
E
AA
¬−
Λ
2
 
E
C
________________________________________________________________________________________ 
 
Prof. Sérgio Gorender Lógica 
 Quantificador Universal: 
• Na regra de introdução x é um elemento 
arbitrário qualquer. P(x) não deve depender 
de qualquer suposição na qual x ocorra. 
• Na eliminação, se P é válido para qualquer 
elemento x, então será válido para um 
elemento específico t. 
 Quantificador Existencial: 
• Na introdução, se P é válido para um 
elemento a, do domínio, então existe um x 
para o qual P(x) é verdade. 
∀−
∀
I
xPx
xP
)(.
)(
∀−
∀
E
tP
xPx
)(
)(.
∃−
∃
I
xPx
aP
)(.
 )(
∃−
∃
E
C
CxPx
tP
 )(.
)]([ 
________________________________________________________________________________________ 
 
Prof. Sérgio Gorender Lógica 
• Na eliminação supõe-se P(t), sendo t uma 
nova variável, instanciando os elementos do 
domínio de x, de forma que t representa 
sucessivamente todos os elementos deste 
domínio. Se P(t) procede, e desta suposição 
se chega a uma fórmula C, que não contém t e 
não depende de nenhuma suposição que 
contenha t, então se tem a prova de C 
independente da suposição de P(t). t não pode 
ocorrer livre em C. 
• Existe uma analogia entre o Quantificador 
Existencial e o Conectivo da Disjunção, uma 
vez que o primeiro é uma generalização do 
segundo. 
• Esta mesma analogia existe entre o 
Quantificador Universal e o Conectivo da 
Conjunção. 
________________________________________________________________________________________ 
 
Prof. Sérgio Gorender Lógica 
 Formas normais. 
 Forma Clausal – forma na qual as declarações 
devem ser escritas para aplicar a resolução. 
 Forma Normal Prenex – fórmula P na forma 
Q(M) onde Q (o prefixo de P) é uma cadeia de 
quantificadores e M (a matriz de P) é uma 
fórmula sem ocorrências de quantificadores. 
• Uma fórmula da Lógica de Predicados que 
não contém quantificadores é chamada de 
fórmula aberta. 
• Ex: ∀x∃y(p(x,y) → (q(x)∧q(y))) 
 Forma normal conjuntiva – fórmula na forma 
normal prenex na qual a matriz é uma 
conjunção de disjunções de fórmulas atômicas, 
negadas ou não. 
• Ex: ∀x∃y((~p(x,y)∨q(x))∧(~p(x,y)∨q(y))) 
 Cláusula – fórmula bem formada. Escrita na 
forma normal conjuntiva, sem instâncias do 
conectivo ∧. 
________________________________________________________________________________________ 
 
Prof. Sérgio Gorender Lógica 
 Skolemização 
• Substituição dos quantificadores existenciais 
em uma fórmula por símbolos funcionais, 
chamados funções de Skolem. 
• Método de eliminação de quantificadores 
existenciais. 
• O resultado de aplicar a skolemização em 
uma fórmula H é uma fórmula G, sem 
quantificadores existenciais. 
• As fórmulas H e G não são necessariamente 
equivalentes, mas garante-se que H é 
insatisfativel se e somente se G é 
insatisfativel! 
• Substituir a subfórmula ∃y(R), da fórmula Q, 
por R[y/f(x1,...,xn)], onde x1,...,xn é uma lista 
de todas as variáveis livres de ∃y(R) e f é 
qualquer símbolo funcional n-ário (função de 
Skolem) que não ocorre em Q. 
• Se não houver variáveis livres em ∃y(R), 
substituir ∃x(R) por R[y/c], onde c é uma 
constante que não ocorre em Q. 
________________________________________________________________________________________ 
 
Prof. Sérgio Gorender Lógica 
• Existem dois casos para a skolemização: 
1. ∃x Q(x) – 
• Não existem variáveis quantificadas 
universalmente na fórmula antes do 
quantificador existencial. 
• A variável x é substituída na fórmula, 
em todas as suas ocorrências ligadas no 
quantificador existencial, por uma 
nova constante. 
• Assumimos que a constante representa 
o valor que torna Q verdadeiro. 
• Q(a). 
________________________________________________________________________________________ 
 
Prof. Sérgio Gorender Lógica 
2. ∀x∃y P(x,y) – 
• Existem quantificadores universais na 
fórmula antes do quantificador 
existencial. 
• A variável y é substituída por uma 
função de skolem – uma nova função 
definida em termos das variáveis que 
aparecem quantificadas universalmenteantes do quantificador existencial. 
• ∀x P(x, f(x)) 
• Após a fórmula estar na forma prenex deve-se 
eliminar os quantificadores existenciais da 
esquerda para a direita. 
________________________________________________________________________________________ 
 
Prof. Sérgio Gorender Lógica 
• Algoritmo de conversão de uma fórmula para a 
forma clausal: 
1. Se P contiver uma variável livre x, substitua P por 
∃x(P). Repita este passo até que a fórmula não 
tenha variáveis livres. 
2. Elimine todo quantificador ∀x ou ∃x que não 
contenha nenhuma ocorrência livre de x no seu 
escopo. (Elimine todo quantificador 
desnecessário) 
3. Eliminar -> e ≡: A -> B eqüivale a ~A ∨ B 
A ≡ B eqüivale a (~A ∨ B)∧(A ∨ ~B) 
4. Reduzir o escopo de ~: ~(~P) = P - Lei de Morgan 
~∀x(Q) = ∃x(~Q) 
~∃x(Q) = ∀x(~Q) 
~(Q ∧ R) = (~Q ∨ ~R) 
~(Q ∨ R) = (~Q ∧ ~R) 
5. Padronizar variáveis: cada quantificador ligado a 
uma variável diferente. Se houver dois 
quantificadores governando a mesma variável, 
substitua a variável de um deles e todas as suas 
ocorrências livres no escopo do quantificador por 
uma nova variável que não ocorra na fórmula. 
6. Mover quantificadores para a esquerda da fórmula 
– Forma Normal Prenex. 
________________________________________________________________________________________ 
 
Prof. Sérgio Gorender Lógica 
7. Eliminar os quantificadores existenciais – 
substituir cada quantificador existencial por uma 
função de Skolem que forneça o mesmo resultado 
- ∃ - Existe um valor. 
8. Eliminar o prefixo (quantificadores universais) – 
todas as variáveis são quantificadas 
universalmente. 
9. Converter a matriz em uma conjunção de 
disjunções – forma normal conjuntiva - 
propriedade distributiva – (A ∧ B) ∨ C = (A ∨ C) 
∧ (B ∨ C) 
 A ∨ (B ∧ C) = (A ∨ B) ∧ (A ∨ C) 
10. Criar uma cláusula separada para cada 
conjunção. 
11. Padronizar as variáveis – duas cláusulas não 
devem fazer referência a uma mesma variável. 
________________________________________________________________________________________ 
 
Prof. Sérgio Gorender Lógica 
 Teorema de Herbrand – 
• Um conjunto de cláusulas S é insatisfatível se e 
somente se existe um conjunto finito de instâncias 
básicas das cláusulas de S que é insatisfatível. 
• Procedimento de Herbrand – 
 Dado um conjunto S de cláusulas, gere 
sistematicamente todos os conjuntos finitos de 
instâncias básicas de cláusulas em S; 
 Para cada conjunto B gerado, teste se B é 
insatisfatível; 
 Pare com SIM, se B for insatisfatível, e pare 
com NÃO, se não houver novos conjuntos a 
gerar. 
________________________________________________________________________________________ 
 
Prof. Sérgio Gorender Lógica 
• Observações: 
 Sempre para com SIM quando S for realmente 
insatisfatível; 
 Nunca pára quando S for satisfatível e existir 
um conjunto infinito de instâncias básicas de 
cláusulas de S; 
 Sempre pára com NÃO quando S for 
satisfatível mas o conjunto de instâncias básicas 
de cláusulas de S é finito. 
 As cláusulas são comparadas, duas a duas, 
inferindo uma nova cláusula a partir delas. 
• Para que dois predicados possam ser comparados 
seus argumentos precisam ser compatíveis. 
• Unificação – procedimento que compara dois 
literais e verifica se eles podem ser tornados 
idênticos por um conjunto de substituições. As 
substituições devem ser consistentes. 
________________________________________________________________________________________ 
 
Prof. Sérgio Gorender Lógica 
 Resolução – 
• Procedimento de prova que executa em uma única 
operação a série de processos envolvidos no 
raciocínio com declarações em lógica de 
predicados. Baseado no Teorema de Herbrand. 
Produz provas por refutação. (Cálculo) 
 Refutação – prova uma declaração mostrando 
que a negação da declaração produz uma 
contradição em relação às declarações 
conhecidas. 
 
________________________________________________________________________________________ 
 
Prof. Sérgio Gorender Lógica 
• Algoritmo Unificar(L1,L2) 
1. Se L1 e L2 forem ambos constantes ou variáveis, 
então: 
1.1. Se L1 e L2 forem idênticos, então retorne 
NIL. 
1.2. Caso contrário, se L1 for uma variável, então, 
Se L1 ocorrer em L2, retorne [FRACASSO], 
caso contrário retorne (L2/L1). 
1.3. Caso contrário, se L2 for uma variável, então, 
Se L2 ocorrer em L1, retorne [FRACASSO], 
ou retorne (L1/L2). 
1.4. Caso contrário, retorne [FRACASSO]. 
2. Se os símbolos do predicado original em L1 e L2 
não forem idênticos, então retorne [FRACASSO]. 
3. Se L1 e L2 tiverem um número diferente de 
argumentos, então retorne [FRACASSO]. 
4. Atribua NIL a SUBST. (Ao final deste 
procedimento, SUBST conterá todas as 
substituições usadas para unificar L1 e L2.) 
5. De i ← 1 para número de argumentos em L1: 
5.1. Chame Unificar com o i-ésimo argumento de 
L1 e com o i-ésimo argumento de L2, 
colocando o resultado em S. 
________________________________________________________________________________________ 
 
Prof. Sérgio Gorender Lógica 
5.2. Se S contém FRACASSO, então retorne 
[FRACASSO]. 
5.3. Se S não for igual a NIL, então: 
5.3.1. Aplique S ao que resta em L1 e L2. 
5.3.2. SUBST := JUNTAR(S,SUBST). 
6. Retorne SUBST. 
 Exemplo de unificação: 
Odeia(x,y) 
Odeia(Marcos, César) 
(Marcos/x,César/y) 
 
________________________________________________________________________________________ 
 
Prof. Sérgio Gorender Lógica 
Algoritmo resolução – 
1.Converta todas as declarações de F para forma 
clausal. 
2.Negue P e converta o resultado para forma clausal. 
Acrescente-o ao conjunto de cláusulas obtido em 1. 
3.Repita até ser encontrada uma contradição, até não 
ser mais possível nenhum progresso, ou até que uma 
quantidade predeterminada de esforço tenha sido 
despendida: 
Selecione duas cláusulas. Chame-as de cláusulas-
pai. 
Resolva as duas juntas. O resolvente será a 
disjunção de todos os literais de ambas as 
cláusulas-pai com a realização das substituições 
apropriadas e com a seguinte exceção: se houver 
um par de literais T1 e ~T2 tal que uma das 
cláusulas-pai contenha T1 e a outra contenha ~T2 e 
se T1 e T2 forem unificáveis, então nem T1 nem T2 
devem aparecer no resolvente. T1 e T2 são 
chamados de literais complementares. Use a 
substituição produzida pela unificação para criar o 
resolvente. Se houver mais de um par de literais 
complementares, apenas um par deve ser omitido 
do resolvente. 
________________________________________________________________________________________ 
 
Prof. Sérgio Gorender Lógica 
Se o resolvente for a cláusula vazia, então uma 
contradição foi encontrada. Se não, acrescente-o 
ao conjunto de cláusulas disponíveis ao 
procedimento. 
 Estratégias que orientam a escolha de cláusulas 
para acelerar o encontro de uma contradição, caso 
ela exista: 
 Resolver apenas os pares de cláusulas que 
contém literais complementares, já que apenas 
estas resoluções produzem novas cláusulas que 
são mais difíceis de satisfazer do que as 
cláusulas-mãe. Indexe as cláusulas pelos 
predicados que elas contêm, indicando se o 
predicado é negado. Depois, dada uma 
determinada cláusula, possíveis resolventes que 
contêm uma ocorrência complementar de um de 
seus predicados podem ser localizados 
diretamente. 
 Elimine certas cláusulas assim que elas forem 
geradas para que não participem de resoluções 
posteriores. Dois tipos de cláusula devem ser 
eliminados: tautologias (que nunca podem ser 
satisfeitas) e cláusulas que estão subordinadas a 
outras cláusulas (isto é, é mais fácil satisfazê-
las. Por exemplo, P ∨ Q está subordinada a P). 
________________________________________________________________________________________Prof. Sérgio Gorender Lógica 
 Sempre que possível, resolva uma das cláusulas 
que seja parte da declaração que estamos 
tentando refutar, ou uma cláusula gerada pela 
resolução desse tipo de cláusula. Esta estratégia 
é chamada de estratégia do conjunto de apoio e 
corresponde à intuição de que a contradição que 
estamos procurando precisa envolver a 
declaração que estamos tentando provar. 
Qualquer outra contradição diria que as 
declarações nas quais acreditávamos 
anteriormente eram inconsistentes. 
 Sempre que possível, resolva cláusulas que 
tenham um único literal. Tais resoluções geram 
novas cláusulas com menos literais do que a 
maior de suas cláusulas-pai e, assim, 
provavelmente estão mais perto do objetivo de 
um resolvente com zero termos. Esse método é 
chamado de estratégia da preferência unitária. 
 
 
 
 
 
 
________________________________________________________________________________________ 
 
Prof. Sérgio Gorender Lógica 
• Exemplo de resolução na Lógica de Predicados: 
Homem(Marcos) 
Pompeano(Marcos) 
~Pompeano(x1) ∨ Romano(x1) 
Soberano(César) 
~Romano(x2) ∨ Leal_A(x2,César) ∨ Odeia(x2,César) 
Leal_A(x3,f1(x3)) 
~Homem (x4) ∨ ~Soberano(y1) ∨ 
~Tenta_Assassinar(x4,y1) ∨ ~Leal_A(x4,y1) 
Tenta_Assassinar(Marcos,César) 
? Odeia(Marcos,César) 
	Lógica de Predicados de Primeira Ordem
	todo o a é um b
	A é um a
	A é um b
	Símbolo de igualdade: =
	F, em caso contrário
	F, em caso contrário
	V, em caso contrário
	? Odeia(Marcos,César)