Linguagens de Programação - Linguagem Prolog - Cláusulas Horn, Unificação e Backtracking

Prévia do material em texto

Cla´usulas Horn Unificac¸a˜o Backtracking
Linguagem Prolog
Cla´usulas Horn, Unificac¸a˜o e Backtracking
Universidade de Bras´ılia
Rodrigo Bonifa´cio
17 de maio de 2011
Cla´usulas Horn Unificac¸a˜o Backtracking
Essa parte do curso e´ baseada no material “Artificial Intelligence
Programming in Prolog”, desenvolvido por Tim Smith, Escola de
Informa´tica, Universidade de Edingburgh.
Cla´usulas Horn Unificac¸a˜o Backtracking
Da mesma forma que as linguagens funcionais se fundamentam na
teoria do λ− calculus, as linguagens do paradigma lo´gico sa˜o
fundamentadas no ca´lculo de predicados de primeira ordem
(first-order predicate calculs)
Cla´usulas Horn Unificac¸a˜o Backtracking
Lo´gica de predicados
Sintaxe
constantes: haskell, prolog, java,. . .
varia´veis: X, Y, Z
predicados: paradigma(haskell, funcional), . . .
operadors: ¬,∨,∧,⇒, ⇐⇒
quantificadores: ∀, ∃
delimitadores: (p ∧ q) ∨ ¬r ⇒ c
Cla´usulas Horn Unificac¸a˜o Backtracking
1 Toda linguagem funcional e´ declarativa
2 Haskell e´ uma linguagem funcional
Cla´usulas Horn Unificac¸a˜o Backtracking
1 Toda linguagem funcional e´ declarativa
2 Haskell e´ uma linguagem funcional
Aplicando regras simples de racioc´ınio, algumas concluso˜es podem
ser derivadas de sentenc¸as como (i) e (ii), por exemplo:
Cla´usulas Horn Unificac¸a˜o Backtracking
1 Toda linguagem funcional e´ declarativa
2 Haskell e´ uma linguagem funcional
Aplicando regras simples de racioc´ınio, algumas concluso˜es podem
ser derivadas de sentenc¸as como (i) e (ii), por exemplo:
Haskell e´ uma linguagem declarativa
Para um computador lidar com sentenc¸as como (1) e (2) e derivar
concluso˜es, uma sintaxe precisa ser bem definida
Cla´usulas Horn Unificac¸a˜o Backtracking
1 Toda linguagem funcional e´ declarativa
2 Haskell e´ uma linguagem funcional
Aplicando regras simples de racioc´ınio, algumas concluso˜es podem
ser derivadas de sentenc¸as como (i) e (ii), por exemplo:
Haskell e´ uma linguagem declarativa
Para um computador lidar com sentenc¸as como (1) e (2) e derivar
concluso˜es, uma sintaxe precisa ser bem definida, e ainda mais
importante as regras de racioc´ınio precisam ser cuidadosamente
formalizadas.
Cla´usulas Horn Unificac¸a˜o Backtracking
Cla´usulas Horn
Cla´usulas Horn Unificac¸a˜o Backtracking
Forma normal clausal
Qualquer predicado lo´gico pode ser escrito na forma normal clausal:
P1 ∧ P2 ∧ . . .PN ⇒ Q1 ∨ Q2 ∨ . . .QM
Onde cada Pi e Qj sa˜o termos.
Cla´usulas Horn Unificac¸a˜o Backtracking
Forma normal clausal
Qualquer predicado lo´gico pode ser escrito na forma normal clausal:
P1 ∧ P2 ∧ . . .PN ⇒ Q1 ∨ Q2 ∨ . . .QM
Onde cada Pi e Qj sa˜o termos. Exemplos de sentenc¸as traduzidas
para forma normal sa˜o:
Predicado Forma clausal
A⇒ B A⇒ B
A ∧ B A ∧ B ⇒ true
A ∨ B true ⇒ A ∨ B
¬A A⇒ false
A ∧ ¬B ⇒ C A⇒ B ∨ C
Lembrando que P ⇒ Q e´ equivalente a ¬P ∨ Q.
Cla´usulas Horn Unificac¸a˜o Backtracking
Nota:
Existem algoritmos que transformam sentenc¸as
proposicionais na correspondente forma normal
clausal
Cla´usulas Horn Unificac¸a˜o Backtracking
Nota:
Existem algoritmos que transformam sentenc¸as
proposicionais na correspondente forma normal
clausal, isso na˜o sera´ exigido no curso.
Importante saber provar que duas sentensa˜o sa˜o iguais.
Finalmente, existem outras formas normais, como a forma
normal conjuntiva, que sa˜o mais eficientes para testes de
satisfabilidade.
Cla´usulas Horn Unificac¸a˜o Backtracking
. . . retornando,
A sintaxe das sentenc¸as na forma normal clausal sa˜o relativamente
complexas:
P1 ∧ P2 ∧ . . .PN ⇒ Q1 ∨ Q2 ∨ . . .QM
Linguagens lo´gicas consideram M no intervalo entre 0 e 1.
Cla´usulas Horn Unificac¸a˜o Backtracking
. . . retornando,
A sintaxe das sentenc¸as na forma normal clausal sa˜o relativamente
complexas:
P1 ∧ P2 ∧ . . .PN ⇒ Q1 ∨ Q2 ∨ . . .QM
Linguagens lo´gicas consideram M no intervalo entre 0 e 1. Ou
seja, estamos interessados em sentenc¸as como:
fatos (M = 0): P1 ∧ P2 ∧ . . .PN
predicados (M = 1): P1 ∧ P2 ∧ . . .PN ⇒ Q
Cla´usulas Horn Unificac¸a˜o Backtracking
. . . retornando,
A sintaxe das sentenc¸as na forma normal clausal sa˜o relativamente
complexas:
P1 ∧ P2 ∧ . . .PN ⇒ Q1 ∨ Q2 ∨ . . .QM
Linguagens lo´gicas consideram M no intervalo entre 0 e 1. Ou
seja, estamos interessados em sentenc¸as como:
fatos (M = 0): P1 ∧ P2 ∧ . . .PN
predicados (M = 1): P1 ∧ P2 ∧ . . .PN ⇒ Q
Fatos e predicados como os descritos aqui sa˜o chamados de
Cla´usulas Horn.
Cla´usulas Horn Unificac¸a˜o Backtracking
Considere as sentenc¸as em lo´gica de predicados
1 paradigma(haskell , funcional)
2 ∀X (paradigma(X , funcional) ∨ paradigma(X , logico)⇒ declarativa(X ))
Cla´usulas Horn Unificac¸a˜o Backtracking
Considere as sentenc¸as em lo´gica de predicados
1 paradigma(haskell , funcional)
2 ∀X (paradigma(X , funcional) ∨ paradigma(X , logico)⇒ declarativa(X ))
Como inferir que haskell e´ uma linguagem declarativa?
Cla´usulas Horn Unificac¸a˜o Backtracking
Considere as sentenc¸as em lo´gica de predicados
1 paradigma(haskell , funcional)
2 ∀X (paradigma(X , funcional) ∨ paradigma(X , logico)⇒ declarativa(X ))
Como inferir que haskell e´ uma linguagem declarativa?
Regras de infereˆncia
Mecanismo que deriva concluso˜es a partir de um processo de
reescrita (ou simplificac¸a˜o) de fo´rmulas.
Cla´usulas Horn Unificac¸a˜o Backtracking
Regras frequ¨entemente usadas
Modus ponens:
F F ⇒ G
G
Eliminac¸a˜o do quantificador universal:
∀X (F (X ))
F (t)
Regra de introduc¸a˜o para conjunc¸a˜o:
F G
F ∧ G
Cla´usulas Horn Unificac¸a˜o Backtracking
Aplicando as regras ao exemplo
Eliminac¸a˜o do quantificador universal em (2):
paradigma(haskell, funcional) ∨ paradigma(haskell, logico) ⇒ declarativa(haskell))
Cla´usulas Horn Unificac¸a˜o Backtracking
Aplicando as regras ao exemplo
Eliminac¸a˜o do quantificador universal em (2):
paradigma(haskell, funcional) ∨ paradigma(haskell, logico) ⇒ declarativa(haskell))
Modus ponens aplicado a fo´rmula acima e (1), conclui-se que:
declarativa(haskell) e´ verdadeiro
Cla´usulas Horn Unificac¸a˜o Backtracking
Mais um exemplo:
1 ∀X (∀Y (mae(X ) ∧ filho de(Y ,X )⇒ ama(X ,Y )))
2 mae(maria) ∧ filho de(joao,maria)
Como derivar que Maria ama Joa˜o?
Cla´usulas Horn Unificac¸a˜o Backtracking
Mecaˆnica do processo de infereˆncia
Em Prolog, a infereˆncia segue um processo intitulado
Unificac¸a˜o (ou Matching)
Cla´usulas Horn Unificac¸a˜o Backtracking
Mecaˆnica do processo de infereˆncia
Em Prolog, a infereˆncia segue um processo intitulado
Unificac¸a˜o (ou Matching)
Dada uma questa˜o, como declarativa(haskell), a unificac¸a˜o
envolve os seguintes passos:
Cla´usulas Horn Unificac¸a˜o Backtracking
Artificial Intelligence in Prolog, Tim Smith
Cla´usulas Horn Unificac¸a˜o Backtracking
Regras para unificac¸a˜o
Dois termos A e B unificam quando:
Se A e B forem constantes, os valores devem ser iguais.
Cla´usulas Horn Unificac¸a˜o Backtracking
Regras para unificac¸a˜o
Dois termos A e B unificam quando:
Se A e B forem constantes, os valores devem ser iguais.
Se A e B forem predicados da forma A = p1(f1, f2, . . . fn) e
B = p2(g1, g2, . . . gn), A e B unificam se p1 = p2 e ocorrer a
unificac¸a˜o de todos os argumentos.
Cla´usulas Horn Unificac¸a˜o Backtracking
Regras para unificac¸a˜o
Dois termos A e B unificam quando:
Se A e B forem constantes, os valores devem ser iguais.
Se A e B forem predicados da forma A = p1(f1, f2, . . . fn) e
B = p2(g1, g2, . . . gn), A e B unificam se p1 = p2 e ocorrer a
unificac¸a˜o de todos os argumentos.
Uma varia´vel unifica com qulquer outro termo. Se B possuir um
valor,a varia´vel A e´ instanciada com aquele valor (e vice-versa).
Ocorre uma associac¸a˜o quando A e B forem ambas varia´veis, de tal
forma que se uma delas for instanciada pelo processo de unificac¸a˜o,
a outra sera´ instanciada com o mesmo valor.
Cla´usulas Horn Unificac¸a˜o Backtracking
Exemplos:
Quais dos seguintes testes unificam?
?− f r e d = X.
?− c = l e t t e r ( c ) .
?− f ( t e e ) = f (S ) .
?− f a t h e r ( john , tom) = f a t h e r ( tom , Who) .
?− c e n t r e ( a , X, c ) = c e n t r e (Y, b , c ) .
?− c o l o u r (N, N) = co l o u r ( green , X ) .
?− f i r s t ( sue , dave , bob ) = f i r s t (N, dave , N) .
Cla´usulas Horn Unificac¸a˜o Backtracking
Obtendo mu´ltiplas respostas
Na u´ltima aula, algo aparentemente saiu errado:
Welcome to SWI−Pro log ( Mult i−th readed , 64 b i t s , Ve r s i on . . . )
Copy r i gh t ( c ) 1990−2010 U n i v e r s i t y o f Amsterdam , VU
Amsterdam SWI−Pro log comes wi th ABSOLUTELY NO WARRANTY.
This i s f r e e so f twa r e , and you a r e welcome to r e d i s t r i b u t e
i t under c e r t a i n c o n d i t i o n s . P l e a s e v i s i t
h t tp : //www. swi−p r o l o g . org f o r d e t a i l s .
?−
?− a n c e s t r a l ( j ava , X ) .
X = cpp ;
X = sm a l l t a l k ;
X = s imu l a ;
ERROR: Out o f l o c a l s t a c k
Cla´usulas Horn Unificac¸a˜o Backtracking
. . . onde t´ınhamos
ancestral(haskell, miranda).
ancestral(miranda, lisp).
ancestral(java, cpp).
ancestral(cpp, smalltalk).
ancestral(smalltalk, simula).
ancestral(X,Z) :- ancestral(X,Y), ancestral(Y,Z).
Cla´usulas Horn Unificac¸a˜o Backtracking
. . . onde t´ınhamos
ancestral(haskell, miranda).
ancestral(miranda, lisp).
ancestral(java, cpp).
ancestral(cpp, smalltalk).
ancestral(smalltalk, simula).
ancestral(X,Z) :- ancestral(X,Y), ancestral(Y,Z).
Isso ocorre devido ao mecanismo de Backtracking, que permite ao
Prolog testar, sempre que poss´ıvel, novas possibilidades quando
uma falha ocorrer.
Cla´usulas Horn Unificac¸a˜o Backtracking
No caso particular, precisamos interromper a
execuc¸a˜o quando na˜o uma linguagem for a raiz da
hierarquia
Cla´usulas Horn Unificac¸a˜o Backtracking
No caso particular, precisamos interromper a
execuc¸a˜o quando na˜o uma linguagem for a raiz da
hierarquia
raiz hierarquia(lisp).
raiz hierarquia(simula).
ancestral(X , ) : −raiz hierarquia(X ), break .
Cla´usulas Horn Unificac¸a˜o Backtracking
No caso particular, precisamos interromper a
execuc¸a˜o quando na˜o uma linguagem for a raiz da
hierarquia
raiz hierarquia(lisp).
raiz hierarquia(simula).
ancestral(X , ) : −raiz hierarquia(X ), break .
Existem outros predicados definidos no Prolog, ale´m do break.
Cla´usulas Horn Unificac¸a˜o Backtracking
No caso particular, precisamos interromper a
execuc¸a˜o quando na˜o uma linguagem for a raiz da
hierarquia
raiz hierarquia(lisp).
raiz hierarquia(simula).
ancestral(X , ) : −raiz hierarquia(X ), break .
Existem outros predicados definidos no Prolog, ale´m do break.
Note que a ordem em que os predicados esta˜o definidos e´
relevante.
Cla´usulas Horn Unificac¸a˜o Backtracking
No caso particular, precisamos interromper a
execuc¸a˜o quando na˜o uma linguagem for a raiz da
hierarquia
raiz hierarquia(lisp).
raiz hierarquia(simula).
ancestral(X , ) : −raiz hierarquia(X ), break .
Existem outros predicados definidos no Prolog, ale´m do break.
Note que a ordem em que os predicados esta˜o definidos e´
relevante. E´ uma boa pra´tica declarar os fatos antes das
regras.
	Cláusulas Horn
	Unificação
	Backtracking