Cap13 - Lógica de Primeira Ordem

Prévia do material em texto

Lógica de Primeira Ordem ( Cálculo dos Predicados) 
 
A Lógica Sentencial (cálculo proposicional) é uma importante ferramenta para se realizar 
inferências sobre fórmulas proposicionais bem formadas. No entanto, ela não é suficiente forte 
para representar certas proposições (sentenças) da linguagem natural e, portanto, não possui 
ferramentas para raciocinar com estas linguagens. 
Por exemplo, é impossível encontrar um caminho formal no cálculo proposicional para 
testar a correção do seguinte argumento: 
 
 Todo professor de ciência da computação possui um computador. 
(1) Sócrates não possui um computador. 
 Logo, Sócrates não é um professor de ciência da computação. 
 
Para que seja possível formalizar este argumento se faz necessário, primeiro, quebrar as 
sentenças em partes de modo que as palavras do conjunto {Todo, possui, não} sejam 
corretamente interpretadas. 
Considerando S: “x possui um computador” vê-se que S não é uma proposição, pois o 
valor verdade de S depende de x. No entanto, se fizermos x = Sócrates então S torna-se uma 
proposição, pois, um dos valores V ou F pode ser associado a S. 
Do ponto de vista das linguagens naturais, um predicado é uma parte da sentença que 
estabelece uma propriedade ao sujeito e contém um verbo. Do ponto de vista da lógica um 
predicado é uma relação e se fizermos p(x) significando ‘ x possui um computador’ então p é 
um predicado que descreve a relação de possuir um computador. Se substituirmos a variável x 
por um nome próprio ou por algum valor definido então se obtém uma proposição. 
Na linguagem comum e na própria matemática, existe uma imensa lista de predicados, 
por exemplo: 
 
a) < ( x, y) é um predicado e se fizermos x=2 e y =3 temos <(2, 3) uma proposição 
verdadeira e <(3,2) uma proposição falsa em N. 
b) Pai(x,y) é um predicado que significa uma relação familiar entre os seres humanos desde 
que x e y sejam ambos humanos. 
 
Desta forma, se p(x) significa que x é mamífero então a proposição p(jacaré) é falsa e 
p(baleia) é verdadeira. De modo análogo a proposição: 
 
 p(baleia) v p(jacaré) v p(pato) v p(boi) v p(cabra) 
 
é verdadeira , daí, podemos dizer que: 
 
‘ existe um elemento no conjunto {baleia, jacaré, pato} tal que p(x) é verdadeira’. 
 
Ou de modo mais formal, seja D= {baleia, jacaré, pato} então podemos dizer que: 
 
 ‘ Existe x ∈D tal que p(x) é verdadeira’. (*) 
 
A representação simbólica para (*) em lógica é dada por: 
 ∃x p(x) 
e o símbolo ∃x é denominado quantificador existencial. 
 
Agora, seja a seguinte proposição p(baleia) & p(boi) & p(cabra) e o seguinte conjunto D = 
{baleia, boi, cabra} então podemos dizer: 
 ‘ Para todo x∈D, p(x) é verdadeira’. (**) 
 A expressão (**) em lógica é representada simbolicamente por: 
 ∀ x p(x) 
e ∀ x é denominado quantificador universal. 
 
O argumento em (1) pode ser representado simbolicamente por: 
 
 ∀ x (professor(x) == > possui_comp(x)) 
 ~ possui_comp(sócrates) 
 ~professor(sócrates) 
 
A noção de quantificador pertence á lógica de primeira ordem ou lógica dos predicados de 
primeira ordem. O termo ‘primeira ordem’ refere-se ao fato dos quantificadores só poderem 
quantificar variáveis que ocorrem nos predicados. 
Da mesma forma que fizemos para o cálculo proposicional é necessário dar uma descrição 
precisa para as fórmulas bem formadas de primeira ordem assim como seus significados. 
 
1 - Sintaxe das Linguagens de Primeira Ordem 
 
Nas linguagens de primeira ordem os termos denotam indivíduos do domínio de 
discurso. Por exemplo, se considerarmos o domínio como sendo o conjunto dos números 
naturais então: 
• 1,2, 3.... são termos 
• +(2, 3), .(1,1) são termos 
pois denotam elementos do domínio. 
 
 
Definição 1- Um alfabeto de primeira ordem A consiste de: 
i. Símbolos lógicos: 
 - pontuação: ( , ) 
 - conectivos: ~(negação), v (disjunção), & (conjunção), == > (condicional), < ==> 
(bi-condicional) 
 - quantificadores: ∀ ( quantificador Uuniversal) 
 ∃ ( quantificador Existencial) 
 - variáveis: um conjunto não vazio, enumerável, de símbolos distintos dos demais. 
 - símbolo de igualdade ( opcional) : = 
 
ii. Símbolos não lógicos: 
 - um conjunto possivelmente vazio de constantes. 
 
 - para cada n > 0, um conjunto, possivelmente vazio, de símbolos funcionais n-ários 
distintos dos demais. 
 
 - para cada n>0, um conjunto, possivelmente vazio, de símbolos predicativos n-
ários distintos dos demais. 
 
Definição 2 – O conjunto dos termos de primeira ordem sobre um alfabeto de primeira 
ordem A é o menor conjunto satisfazendo as seguintes condições: 
 
i) toda variável em A é um termo; 
ii) toda constante em A é um termo sobre A; 
iii) se 1 2, ,..., nt t t são termos sobre A e f é um símbolo funcional n-ário de A, então 
f( 1 2, ,..., nt t t ) também é um termo sobre A 
 
Definição 3 - O conjunto de fórmulas sobre um alfabeto de primeira ordem A é o menor 
conjunto satisfazendo às seguintes condições: 
 
i) se 1 2, ,..., nt t t são termos sobre A e p é um símbolo predicativo n-áriode A, então 
p( 1 2, ,..., nt t t ) é uma fórmula sobre A, chamada fórmula atômica. 
 
ii) se 1 2t e t são termos sobre A e ‘=’ é um símbolo de A então ( 1 2t t= ) é uma 
fórmula sobre A, também chamada fórmula atômica. 
 
 
iii) se p e q são formulas sobre A, então (~p), (p & q), (p v q), ,(p == >q) e 
 (p< ==>q) também são fórmulas sobre A. 
 
iv) se p é uma fórmula sobre A e x é uma variável de A então∀ x p(x) e ∃ x p(x) são 
fórmulas sobre A. 
 
Definição 4 - Uma fórmula q é uma sub-fórmula de uma fórmula p se e somente se q for p 
ou q ocorre em p. 
 
Definição 5 – A linguagem de primeira ordem sobre um alfabeto de primeira ordem A, 
denotada por L(A), é o conjunto de termos e fórmulas de primeira ordem sobre A. 
 
Como nas linguagens proposicionais nas formulas de primeira ordem também são 
utilizados parênteses para hierarquizar o processo de avaliação da fórmula. 
 
Considere o alfabeto de primeira ordem a contendo como símbolos não lógicos: 
 
constante: ‘1’ 
símbolos funcionais unários: ‘-‘ e ‘sen’ 
símbolo predicativo binário: ‘≤ ’ 
 
Podemos transformar a sentença : ‘ Para todo x , -1≤ senx ≤ 1` em uma fórmula de L(A) 
como ∀x(≤ (−(1),SEN(x))& ≤ (SEN(x),1)) 
 
Definição 6 - 
a) Em uma fórmula da forma ´∀x(Q)´ou '∃x(Q)' , Q é o escopo do quantificador 
´ ´ ' 'x ou x∀ ∃ 
b) Uma ocorrência de uma variável x em uma fórmula P é ligada em P se a ocorrência se dá 
em uma subfórmula de P da forma ´∀x(Q)´ou '∃x(Q)' , caso contrário a ocorrência de x é livre 
e dizemos que x é livre em P. 
c) Uma fórmula P é uma sentença (fechada) se nenhuma variável livre ocorre em P. 
 
Exemplo 1 - Seja a fórmula P = ´∀x(Q(x, y)' então pela definição 6 tem-se que a variável x 
ocorre ligada em P e também P não é uma sentença por que a variável y ocorre livre em P. 
 
A noção de substituição de variáveis por termos é extremamente importante para a 
realização de inferências em lógica de primeira ordem. 
É interessante observar que no cálculo proposicional não existem termos e as únicas 
variáveis utilizadas são as variáveis proposicionais que são úteis para descrever certas situações 
ou estado de coisas em um certo mundo. Cada variável proposicional exprime um fato. 
 
Definição 7 – Se u é um termo então u[x/t] denotará o termo obtido substituindo-se cada 
ocorrência de x em u pelo termo t.Se P é uma fórmula então P[x/t] denotará a fórmula obtida 
substituindo-se cada ocorrência livre de x em P pelo termo t. Se 1 2, ,..., nx x x são variáveis 
distintas e 1 2, ,..., nt t t são termos, a expressão 1 1 2 2[ / , / ,..., / ]n nu x t x t x t denotará a substituição 
simultânea de ix por it , i = 1,2,...,n, no termo u e de fórmula análoga para fórmulas. Uma 
variável x é substituível por t em uma fórmula P se, para cada variável y ocorrendo em t, 
nenhuma subfórmula de P da forma ´∀y(Q)´ou '∃y(Q)' contém uma ocorrência livre de x. 
 
2 - Semântica das Linguagens de Primeira Ordem 
 
Até aqui uma fórmula é uma seqüência de símbolos sem qualquer significado associado. 
Para que uma fórmula tenha significado, devemos dar alguma interpretação para seus símbolos 
de modo que a fórmula possa então ser avaliada em valores V ou F. 
 
Definição 8 - Uma interpretação para uma fórmula bem formada wff consiste de um 
conjunto não vazio D denominado domínio da interpretação, junto com uma atribuição que 
associa os símbolos da wff a valores de D, da seguinte forma: 
 
a) Para cada símbolo predicativo é atribuído uma relação de D. 
b) Para cada símbolo funcional é atribuído uma função de D. 
c) Para cada variável livre é atribuído um valor de D. Todas as ocorrências de uma variável 
livre x é atribuído um mesmo valor de D. 
d) Para cada constante é atribuído um valor de D. Todas as ocorrências da mesma constante 
recebem o mesmo valor. 
 
Com esta definição de interpretação, temos os ingredientes necessários para que possamos 
definir a semântica das fórmulas de primeira ordem. Informalmente, o significado de uma 
fórmula será verdadeiro ou falso dependendo como a interpretação foi definida. Porém como 
estamos considerando quantificadores então necessitamos fazer uma definição precisa de como 
encontrar o valor verdade de uma formula bem formada. 
 
Definição 9 - O significado de uma fórmula bem formada com respeito a uma 
interpretação com domínio D é o valor verdade obtido por aplicar as seguintes regras: 
 
1- Se na fórmula não ocorre quantificadores então seu significado é o valor verdade da 
proposição obtida através da aplicação da interpretação na fórmula. 
 
2- Se na fórmula ocorre o quantificador Universal, então o significado de xP∀ é verdade se 
P(u[x/d]) é verdade para todo d D∈ . Caso contrário o significado é falso. 
 
3- Se na fórmula ocorre o quantificador Existencial, então xP∃ é verdade se P[u(x/d)] é 
verdade para algum d D∈ . Caso contrário é falso. 
 
Quando uma fórmula P é verdadeira (ou falsa) com respeito a uma interpretação I, 
diremos que P é verdadeira (ou falsa) para I. 
 
Exemplo 2 - 
a) Todo homem fala uma língua : ∀x∃y( fala(x, y) = V 
b) Uma língua é falada por todos os homens: ∃y∀x( fala(x, y) = F 
 
Exemplo 3 – Vamos considerar o predicado ‘é-pai-de(x,y)’ significando ‘x é pai de y’. O 
domínio de nossa interpretação é o conjunto de todas as pessoas vivas ou mortas. Suponha que 
João é pai de Maria. As seguintes fórmulas possuem significados: 
 
 ∃x(é − pai− de(x,maria) = V 
 
 ∀x∃y(é − pai− de(x, y)) = F 
 
 ∃x∀y(é − pai− de(x, y)) = F 
 
 ∀y∃x(−e− pai− de(x, y)) = V 
 
Definição 10 - Uma interpretação I é um modelo para uma fórmula bem formada P se P 
é verdadeira com respeito aquela interpretação. 
 
2.1- Validade 
 
Existem fórmulas bem formadas que são verdadeiras para qualquer interpretação? 
Sim, e neste caso dizemos que a fórmula é válida, consequentemente, uma fórmula é 
válida se qualquer interpretação é um modelo para ela. Caso contrário, a fórmula é inválida. 
Uma fórmula é insatisfazível se ela é falsa para todas as possíveis interpretações, portanto 
não possui modelo. No entanto, se existir um modelo para ela a fórmula é satisfazível. 
Assim, uma fórmula de primeira ordem bem formada P pode ser caracterizada da 
seguinte forma: 
 
a) P é uma tautologia, se ela é válida e satisfatível, 
b) P é contingente se ela é satisfatível e inválida, e 
c) P é contraditória se ela é insatisfatível e inválida. 
 
Usualmente as fórmulas válidas de um sistema lógico são denominadas teoremas. 
Os procedimentos descritos na seção anterior para o cálculo proposicional, por exemplo, 
as tabelas verdades, são chamados procedimentos de prova. 
Um procedimento é completo quando toda fórmula válida pode ser demonstrada ser um 
teorema e correto se todo teorema produzido pelo procedimento de prova for realmente válido. 
É fato conhecido que existe procedimento de prova para a lógica de primeira ordem, mas 
não de decisão, isto significa que não há garantias de que um procedimento de prova 
convergirá para a prova em um número finito de passos quando se tenta demonstrar um não 
teorema. Todavia em termos práticos essa carência não limita a mecanização da lógica. 
Até aqui ainda não apresentamos nenhum sistema de inferência para a lógica clássica o 
fizemos apenas para o cálculo proposicional. Existem vários sistemas lógicos diferentes para a 
realização de inferências de primeira ordem que são corretos e completos. Podemos citar, por 
exemplo, Dedução Natural, que é um sistema bastante potente e conveniente para o contexto 
matemático. 
No entanto, neste curso, estamos interessados na mecanização da Lógica para aplicações 
na formalização e solução de problemas práticos. 
A contribuição mais importante para a mecanização da lógica foi dada por Herbrand em 
1930 ao desenvolver um algoritmo que encontra uma interpretação que pode tornar falsa uma 
fórmula dada. No entanto, se a fórmula dada permanecer válida tal interpretação não existe e o 
algoritmo parará depois de um número finito de tentativas. 
Os procedimentos de Herbrand e o Método da Resolução de Robinson não seguem a 
tradição da prova direta tipo a que é realizada por Dedução natural, mas sim, busca a prova por 
refutação, demonstrando que a negação da fórmula é inconsistente. A idéia destes 
procedimentos baseia-se no principio do terceiro excluído, pois se a negação de uma fórmula é 
falsa então ela é verdadeira. 
Segundo Casanova, um programa em Lógica é um conjunto finito de sentenças que 
descreve um determinado problema ou situação sendo diferente de um programa em Fortran 
ou em C que é a descrição de um algoritmo ou procedimento para resolver um problema. 
Programação em lógica enfatiza a estrutura de um problema e não a construção de um 
procedimento para resolvê-lo. O estilo da programação em Lógica é denominado declarativo 
(não procedimental) em contraste com Programação Procedimental (ou Imperativa) típica das 
linguagens tradicionais. É interessante observar que a programação em Lógica não se limita a 
um exercício de formalização, mas propõe a utilização dos mecanismos da Lógica para resolver 
problemas. 
A programação em Lógica, pelo seu estilo declarativo, se presta sobremaneira ao 
desenvolvimento de Sistemas Baseado em Conhecimento (SBC). 
A pergunta que se faz neste ponto é: Quanto de Lógica precisamos conhecer para que 
possamos desenvolver aplicações práticas, ou, para utilizarmos as linguagens de programação 
em Lógica? 
A resposta óbvia é que quanto mais soubermos de um assunto ou de uma área melhor 
estaremos preparados para obter soluções mais otimizadas ou mais fundamentadas e até 
mesmo mais corretas. Sendo assim, sugerimos que o aluno que se interessar por esta disciplina, 
estude-a com mais profundidade, existem muitos textos interessantes na WEB, livros já 
publicados tanto do ponto de vista introdutório quanto avançado. Sugerimos também que o 
aluno que deseja iniciar em Inteligência Artificial deve começar com Lógica Clássica e Redes 
Neurais. Muitos pesquisadores optam em olhar o mundo apenas em uma direção, porém no 
mundo atual, isto não é mais suficiente. O aluno que tem sua formação nas Engenharias terá 
muitomais facilidades com Redes Neurais e dificuldades com Lógica, e o pessoal da Ciência da 
Computação em geral, tem mais facilidade com programação em Lógica, mas não 
necessariamente em Lógica pura. Isto se dá porque não pertence a nossa cultura o estudo da 
Lógica na formação básica de qualquer aluno da graduação em Engenharia, constando apenas 
no histórico da Ciência da Computação, da Matemática e Filosofia. 
 
Para que possamos realizar inferências utilizando o método de resolução, precisamos 
antes transformar as fórmulas bem formadas em formatos canônicos. 
Para isso, precisamos de algumas definições e alguns resultados que facilitarão bastante a 
obtenção destas formas canônicas. 
 
Resultado 1 - Sejam L uma linguagem de primeira ordem e P, Q e R fórmulas bem 
formadas de L e x uma variável. Então: 
 
i) ( P & ( Q v R)) |=|( ( P & Q) v (P & R)) 
 
ii) ( P v ( Q & R)) |=|( ( P v Q) & (P v R)) 
 
iii) ~(P v Q) |=| (~P & ~Q) 
 
iv) ~(P & Q) |=| (~P v ~Q) 
 
v) ( P == >Q) |=|~P v Q 
 
vi) ~ ∀ x P |= | ∃x ~P 
 
vii) ~∃ x P |=|∀ x~ P 
 
viii) ∀ x P & ∀ x Q |=| ∀ x (P & Q) 
 
ix) ∃x P v ∃x Q |=| ∃x ( P v Q) 
 
x) Se x não ocorre livre em P então 
a) ( P v ∀ x Q) |=| ∀ x (P v Q) 
b) (P v ∃x Q) |=| ∃x (P v Q) 
 
Definição 11 - Dada uma fórmula P o fecho universal de P é a fórmula 
 ∀x1....∀xn (P) 
e o fecho existencial é a fórmula 
 ∃x1...∃xn (P) . 
 
Definição 12 – Uma fórmula P está na forma normal prenex se e somente se P for da 
forma “Q(M)” onde Q, o prefixo de P, é uma cadeia de quantificadores e M, a matriz de P, é 
uma fórmula sem ocorrência de quantificadores. 
Uma fórmula P esta na forma normal conjuntiva (fnc) se e somente se estiver em forma 
normal prenex e a sua matriz for uma conjunção de disjunção de fórmulas atômicas, negadas 
ou não. 
 
Exemplo 4 - A fórmula ∀x∃y(p(x, y) ==> q(x)) está na forma normal prenex e a fórmula 
∀x∃y((~ p(x, y) v q(x)) & (p(x, y)v ~ q(y)))) está na forma normal conjuntiva. 
 
Definição 13 – 
a) Um literal é uma fórmula atômica ou sua negação 
b) Uma cláusula é um conjunto de literais. 
c) Um literal é positivo se e somente se for uma fórmula atômica, caso contrário será 
negativo. 
d) Uma cláusula que não contém literal é denominada cláusula vazia e que será 
representada por [] ou �. 
 
A cláusula vazia representa uma fórmula insatisfazível, por exemplo, ‘ P & ~P ‘. 
 
A Clausula de Horn é uma clausula com no máximo um literal positivo. 
 
Definição 14 — A linguagem de um conjunto de cláusulas S é a linguagem de primeira 
ordem L(S) cujos símbolos não-lógicos são aqueles que ocorrem em S. 
 
Exemplo 5 – Literais e cláusulas 
a) As seguintes expressões são literais: 
 pai(a,y), irmão(b,x), professor(y) 
 
b) O conjunto de literais abaixo denota uma cláusula 
 {pai(a,y), irmão(b,x) , professor(y)} 
 
e que representa a seguinte fórmula 
 
∀x∀y(pai(a, y) ∨ irmão(b, x) ∨ professor(y)) 
 
 
3- Algoritmo da Representação Clausal ( Casanova) 
 
Entrada: uma fórmula P 
Saída: uma representação clausal S para P 
 
a) Tome o fecho existencial de P 
Se P contiver variáveis livres, acrescente um quantificador existencial para cada 
variável livre. 
 
b) Elimine quantificadores redundantes 
Elimine todo quantificador ‘ ' ' 'x ou x∀ ∃ que não contenha nenhuma ocorrência 
livre de x no seu escopo. 
 
c) Renomeie variáveis quantificadas mais de uma vez 
Se houver dois quantificadores governando a mesma variável substitua a variável 
de um deles e todas as ocorrências livres dela no escopo do quantificador por uma nova 
variável que não ocorra na fórmula. Repita o processo até que todos os quantificadores 
governem variáveis diferentes. 
 
d) Elimine os conectivos ‘== >’ e ‘< ==>’ 
 Substitua: 
 Q== > R por ( ~Q v R) 
 
 Q <== > R por ( ~Q v R) & (Q v ~R) 
 
e) Mova ‘~’ para o interior da fórmula 
 
 ~ ∀ x P |=| ∃x ~P 
 
 ~∃x P |=|∀ x~ P 
 ~(P & Q) |=| (~P v ~Q) 
 
 ~(P v Q) |=| (~P & ~Q) 
 
 ~~Q |=| Q 
 
até que cada ocorrência de ‘~ ‘ preceda imediatamente uma fórmula atômica. 
 
f) Elimine os quantificadores existenciais 
 
Seja P a fórmula corrente. Crie uma nova fórmula corrente substituindo a 
subfórmula de P da forma ‘∃x(Q) ’ que se situa mais a esquerda por 
 
 Q(y/f( 1 2, ,..., nx x x ) 
onde: 
 
1- 1 2, ,..., nx x x é a lista de todas as variáveis livres de ∃x(Q) ; 
2- f é qualquer símbolo funcional que não ocorre em P; 
3- Repita o processo até que todos os quantificadores existenciais tenham sido 
eliminados; 
4- se não houver variáveis livres substitua ∃x(Q) por Q[x/c], onde c é uma 
constante que não ocorre na fórmula; 
5- os novos símbolos funcionais assim introduzidos são denominados funções de 
Skolem. O processo de substituição é chamado Skolemização. 
 
g) Obtenha a forma normal prenex 
Mova os quantificadores universais para a esquerda. 
 
h) Obtenha a forma normal conjuntiva 
Substitua 
 
 (P v ( Q & R) por ( P v Q) & (P v R) 
 
 ( Q & R) v P por (Q v P ) & (R v P) 
 
 Até que a matriz da fórmula seja uma conjunção de disjunções 
 
i) Obtenha a representação clausal 
A representação clausal S de P será o conjunto das cláusulas que representam as 
disjunções de literais da matriz da fórmula resultante do passo anterior. 
 
Exemplo 6: Seja a fórmula ∀x∀y(menor(x, y) ==> ∃z(igual(soma(x, z), y))) 
 
a) não há variáveis livres 
b) não há quantificadores redundantes 
c) não necessita renomear variáveis 
d) eliminação dos conectivos (== >) 
 
 ∀x∀y(~ menor(x, y) v ∃z(igual(soma(x, z), y))) 
e) não há necessidade de mover ‘~’ para o interior da fórmula 
f) eliminação dos quantificadores existenciais 
 
 ∀x∀y(~ menor(x, y) v (igual(soma(x, f (x, y)), y))) 
 
g) já esta na forma prenex 
h) forma conjuntiva 
 
 (~ menor(x, y) v (igual(soma(x, f (x, y)), y))) 
 
i) representação clausal 
 
 {~ menor(x, y), igual(soma(x, f (x, y)), y)} 
 
Definição 15 - Um conjunto de cláusulas S é uma representação clausal para uma 
fórmula P se e somente se 
 P é satisfazível se e somente se S é satisfazível. 
 
Um conjunto de cláusulas S é insatisfazível se for falsa para todas as interpretações em 
todos os domínios. Como a análise de todas as interpretações é inviável, seria muito 
conveniente fixar-se um domínio especial no qual S seja insatisfazível se e somente se for falsa 
em todas as interpretações. A este domínio especial denominaremos Universo de Herbrand e 
será denotado H. 
 
 
4- Principio da Resolução 
 
Teorema de Herbrand: Se S for um conjunto de cláusulas tal que seja falsa para toda 
interpretação I de Herbrand, então S é insatisfazível para qualquer domínio. 
 
O Teorema de Herbrand permite, com uso de árvores semânticas, decidir se um conjunto 
de cláusulas dadas é insatisfazível. Porém, como esta árvore cresce exponencialmente, 
dependendo das cláusulas em questão, a quantidade de elementos envolvidos pode superar a 
capacidade de armazenamento dos maiores computadores existentes, o que a torna 
impraticável. 
Para evitar esta excessiva geração de elementos, Robinson estabeleceu em 1965 outro 
algoritmo que pode ser aplicado diretamente sobre qualquer conjunto S de cláusulas para 
verificar sua insatisfazibilidade – O princípio da resolução. 
 
A idéia essencial é verificar se S possui a cláusula vazia ou senão, se esta pode ser 
derivada de S. Caso isto ocorra, S é insatisfazível. 
Basicamente este princípio consiste numa extensão do modus ponens, anteriormenteexplorado por Davis e Putnam, segundo o qual, das cláusulas: 
 
C1: P 
C2: ~P v Q 
Pode-se derivar 
C3: Q 
 
Estendendo esta idéia para qualquer par de cláusulas, podemos enunciar o princípio da 
Resolução: 
Para qualquer par de cláusulas C1 e C2, se existir um literal L1 de C1 que for 
complementar de outro literal L2 de C2 , então remova L1 de C1 e L2 de C2 e 
construa a disjunção dos remanescentes nas cláusulas. 
A nova cláusula construída é o resolvente de C1 e C2. 
 
Então o procedimento de prova por resolução usa sentenças na forma de cláusulas. 
Inicialmente, os axiomas e a negação do teorema que se deseja provar são convertidos em 
cláusulas. Então novas cláusulas - os resolventes- são deduzidas pela regra de inferência acima. 
O teorema principal do procedimento estabelece que se um resolvente não for satisfazível, 
então nenhum de seus antecedentes o será - o que inclui a negação do teorema inicial. Seu 
objetivo é obter a clausula vazia, ou seja, uma contradição explícita. 
 
Um ponto importante é o processo de unificação. Para unificar dois literais, deve-se 
primeiro verificar se o predicado é o mesmo. Se o for, pode-se prosseguir. Assim, os literais: 
 
 Amigos(Luis, Pedro) 
 Parentes(Luis, Pedro) 
 
não podem ser unificados, pois são predicados diferentes. 
 
Se os predicados combinarem, deve-se testar os argumentos: se o primeiro combina, 
continua-se com o segundo e assim por diante. 
Para testar cada um deles, basta chamar o procedimento de unificação recursivamente; 
funções, predicados ou constantes diferentes não podem combinar; somente se forem idênticos. 
Uma variável pode se combinar com outra, uma constante, uma função ou expressão 
predicativa, com restrição que estas duas últimas não devem conter quaisquer instancias das 
variáveis sendo comparadas. 
 
O alvo deste procedimento é descobrir ao menos uma substituição que causa igualdade de 
dois literais. Em geral, se houver uma tal substituição, haverá muitas. 
 
Agora já se tem elementos para julgar se dois literais são contraditórios, isto é, se um deles 
pode ser unificado com a negativa do outro. 
Assim, homem(x) e ~homem(Maria) são contraditórios uma vez que podem ser unificados. 
 O correspondente intuitivo para este fato é que não pode ser verdade que para todo x que 
homem(x) se for conhecido para algum x, digamos Maria, para o qual homem(x) for falso. 
 
Logo, para se utilizar resolução para expressões em lógica de primeira ordem, deve-se 
utilizar o algoritmo de unificação para localizar pares de literais que podem ser cancelados. 
Será preciso utilizar o produto deste algoritmo para gerar cláusulas resolventes. Por 
exemplo, suponha que se deseje resolver: 
 
1- homem(Pedro) 
2- ~homem(x) v mortal(x) 
 
O literal homem(Pedro) pode ser unificado com o literal homem(x) com a substituição 
Pedro/x. Não se pode cancelar os dois resolventes como em lógica proposicional e obter o 
resolvente mortal(x), pode-se apenas concluir mortal(Pedro). 
Logo, o resolvente gerado por 1 e 2 deve ser mortal(Pedro). 
 
É importante observar que se ocorrerem duas instâncias de uma mesma variável, elas 
devem ser submetidas à mesma substituição. 
 
De modo mais formal, uma substituição é um conjunto finito da forma: 
 
 � = {t1/v1, t2/v2, ...,tn/vn} 
 
onde cada vi é uma variável e cada ti um termo sendo que não mais de um elemento do 
conjunto pode conter uma mesma variável após a barra. 
Duas clausulas C1 e C2 são unificáveis se existir uma substituição � tal que C1 � = C2 �. 
Se C’ = C � para qualquer �, então C’ será uma instância de C. 
 
Uma substituição � chama-se unificador mais geral (umg) de duas claúsulas C1 e C2 se e 
somente se: 
 
1) C1 � = C2 �; e 
2) Para qualquer outro unificador �’, C1 �’ = C2 �’ será uma instância de C1 � = C2 � 
 
Robinson demonstrou que se duas cláusulas forem unificáveis, então existirá o umg para 
elas. O núcleo do processo de resolução é o algoritmo da unificação que determina se ou não 
duas cláusulas podem ser unificáveis e, no caso afirmativo, estabelece o umg. 
Através de um exemplo, vamos resumir os conceitos apresentados até aqui a respeito da 
unificação ao efetuar uma resolução em lógica de primeira ordem. 
 
Exemplo 7: Considerando as seguintes informações 
 
1- Toda atriz é bonita 
2- As avós não são bonitas 
3- Algumas avós são inteligentes 
 
Queremos provar utilizando o processo de resolução com unificação que: 
 
4– Algumas pessoas que são inteligentes não são atrizes 
 
Primeiro vamos representar estas informações numa linguagem de primeira ordem, assim: 
 
1−∀x(atriz(x)→ bonita(x))
2−∀x(avó(x)→~ bonita(x))
3−∃x(avó(x)& inteligente(x))
4−∃x(inteligente(x)& ~ atriz(x))
 
Passamos as sentenças de primeira ordem para forma de cláusulas lembrando de negar a 
quarta, pois queremos prová-la, assim: 
1- ~atriz(x) v bonita(x) 
2- ~avó(y) v ~bonita(y) 
3- avó(a) & inteligente(a) 
4- avó(a) ........ simp - 3 
5- inteligente(a) ........ simp - 3 
6- ~inteligente(z) v atriz(z) ................. negação de 4 
 
Aplicando resolução 
7- ~inteligente(a) v atriz(a) ......... 6, unificação {a/z} 
8- atriz(a) ......... SD - 7, 5 
9- ~atriz(a) v bonita(a) ................ 1, unificação {a/x} 
10- bonita(a) ................ SD - 8,9 
11- ~avó(a) v ~bonita(a) ................. 2, unificação {a/y} 
12- ~avó(a) ............... SD - 10,11 
13- � ------------ CONJ - 4, 12 ---- contradição 
 
Em ciência da computação, as pesquisas em Lógica Clássica estão mais direcionadas para 
a confecção de linguagens de programação em lógica, representação de conhecimento e 
sistemas especialistas. 
Como já foi dito anteriormente, já existem potentes linguagens de programação em Lógica 
sendo comercializadas, como é o caso do Prolog. Existem também disponível na internet alguns 
protótipos de uso livre para estudantes. A boa notícia é que estas linguagens já estão prontas 
para realização de provas, bastando entrar com as informações em formato de cláusulas e então 
elaborar as perguntas pertinentes a estas informações e aguardar as respostas.