Programação em lógica e lógica
Jacques Robin, DI-UFPE
www.di.ufpe.br/~jr
O que é Prolog?
Primeira e mais divulgada linguagem do paradigma
da Programação em Lógica (PL)
 Operacionalização simples, prática e eficiente da
metáfora da PL
 PL unifica:

• Engenharia de Software (especificação formal, linguagens
de programação)
• Inteligência Artificial (IA) (raciocínio com Formalismos
de Representação do Conhecimento (FRCs))
• Banco de Dados -- Dedutivos (BDDs)
• Teoria Lógica (TL) das provas
Metáfora da programação em lógica
Teoria Lógica = Programa = BD dedutivo = Base de
Conhecimento (BC)
 Programar = apenas declarar axiomas e regras
 Axiomas da TL:

• fatos da BC
• parte extensional do BDD
• dados explícitos de um BD tradicional

Regras da TL (e da BC):
• parte intencional do BDD

Teoremas da TL:
• deduzidos a partir dos axiomas e das regras
• dados implícitos do BDD
Linguagens de PL
Interpretadas (interatividade) e compiladas
(eficiência)
 Interpretadores-Compiladores (IC) de PL:

• SGBD dedutivos (em geral em memória central)
• Motores de inferência
• Provadores de teoremas para lógicas com grande interseção com
a Lógica da 1a ordem (L1)

Interação:
• Declarar o que é verdadeiro (axiomas e regras do PL/BDD)
• Chamar o IC e carregar o PL/BDD
• Perguntar o que é verdadeiro (tentar provar teoremas =
executar o PL = consultar o BDD)
PL x resto do mundo

PL x programação imperativa, funcional e 00:
• mais declarativa, mais alto-nível
• mais versátil -- linguagem única para:



especificar formalmente e implementar
programar aplicações, scripts e consultas em BD
PL x outros FRCs:
• melhor fundamentação teórica
• melhor integração com o resto da ciência computação
PL = base interessante para integração de
paradigmas
 PL = caso particular de programação por restrições

Ciclo de desenvolvimento de um
software baseado em conhecimento
Ontologia
Nível de
Conhecimento
AQUISIÇÃO
Raciocínio
Nível Lógico
FORMALIZAÇÃO
Nível de
Implementação
IMPLEMENTAÇÃO
MANUTENÇÃO
BASE
Raciocínio automático em software
baseado em conhecimento

Propriedades desejáveis:
 R , R ' (( R | R ' )  ( sem ( R ) | sem ( R ' )))
• correto:
 R , R ' (( sem ( R ) | sem ( R ' ))  ( R | R ' ))
• completo:
• composicional:
 R , R1  R N , ((  f ( R  f ( R1 ,  , R N ))
 (  g ( sem ( R )  g ( sem ( R1 ),  , sem ( R N )))))
Programação procedimental
x programação declarativa







1. Escolher linguagem de
especificação formal (LE)
2. Especificar formalmente
os requisitos na LE
3. Escolher linguagem de
programação (LP)
4. Codificar estruturas de
dados na LP
5. Codificar passo a passo
estruturas de controle na
LP
6. Escolher/escrever
compilador da LP
7. Executar programa




Escolher FRC (1,3)
Declarar estruturas de
conhecimento no FRC (2,4)
Escolher/escrever motor
de inferência para FRC (6)
Consultar base de
conhecimento sobre
verdade de um fato (7)
• foi declarado?
• pode ser deduzido?
• reposta:


:booleana (L0, L1)
: instanciação de
variáveis (L1)
L1 como FRC e linguagem de
programação declarativa: motivação

Satisfaz em grande parte para muitas aplicações:
• Adequação representacional e inferencial
• Eficiência aquisicional e inferencial
Propriedades formais (semântica, complexidade da
inferência) muito bem conhecidas
 Referência e interlingüa para comparar FRCs
 Regras de inferências permite RC modular:

• Independência entre regras
• Conclusão desamarrável das premissas: uma vez deduzida,
a justificação de uma conclusão pode ser esquecida
Revisão de L1: sintaxe
Fórmula

|
|
|
|
Fórmula-Atômica
(Fórmula)
 Fórmula
Quantificador Variável, ... Fórmula,
Fórmula Conectivo Fórmula
Fórmula-Atômica
Predicado(Termo,...) | Termo = Termo
Termo

|
|
Função(termo,...)
Constante
Variável
Conectivo
Quantificador
Constante
Variável
Predicado
Função






|||
 |  | !
Wumpus | Agente | Flecha | ...
x | y | wumpus | agente | ...
Adjacente | Vivo | ...
Em | Brisa | ...
Revisão de L1: semântica

Engajamento ontológico:
• universo é dividido em:




objetos, as entidades individuais do universo, representado
pelos termos
propriedades, que distinguem um objeto dos outros,
representados pelas funções
relações entre objetos, representados pelos predicados
Engajamento epistemológico:
• afirmações representadas pelas formulas são:

verdadeiras xorfalsas
• quantificadores e variáveis permitem representar
intencionalmente, propriedades de conjuntos de objetos
• Igualdade semântica permite representar identidade
entre objetos
Revisão de L1: mecanismo de inferência
completo (para verificação)
Fórmula da
lógica de 1a.
ordem
Fórmula na
forma
normal
Conversão para
forma normal
Demodulação
Fórmula
instanciada
ou False
Prova por
Refutação
Resolução
Unificação
Revisão de L1:
forma normal (1)

Def:
L1   N  L1 / N  p1    p n  c1    c m 
I
onde  i , j p i , p j são formulas atómicas
Thm:  F  L1,  N  L1I , N 
 Regras de conversão:

F
• implicação: ( p  q )  (  p  q )
(  ( p  q ))  (  p   q )
• negação:
(  ( p  q ))  (  p   q )
(  (  X , p ( X )))  (  X ,  p ( X ))
(  (  X , p ( X )))  (  X ,  p ( X ))
(  p )  p
• variáveis: ((  X p ( X ))  (  X q ( X )))  ((  X p ( X ))  (  Y q (Y )))
Revisão de L1:
formal normal (2)

Regras de conversão (cont.):
• quantificadores: ( p (Y )  (  X q ( X )))  (  X ( p (Y )  q ( X )))
(  X p ( X ))  p ( a )
• skolemização:
(  Y ,  X p ( X ))  (  Y p ( f (Y , a )))
• distributividade: (( p  q )  r )  (( p  r )  ( q  r ))
• associatividade: (( p  q )  r )  ( p  ( q  r ))  ( p  q  r )
(( p  q )  r )  ( p  ( q  r ))  ( p  q  r )
• disjunções:

(  p   s  q  r )  (( p  s )  ( q  r ))
Quantificação universal implícita
Revisão de L1: refutação,
unificação e substituição
Motivação de provas por refutação:
KB  P





(KB  P)
(KB  P)
(KB   P)
(KB   P)  False
(KB   P)  False
Substituição de variáveis de uma formula f:
conjunto de pares Var/const ou Var1/Var2
Unificação de 2 formulas f e g:
• substituição S das variáveis de f e g tal que S(f)=S(g)
• 2 resultados:


S
r=S(f)=s(g)
Revisão de L1: unificação posicional

Exemplos:
• unif(conhece(joao,X),conhece(Y,leandro)) =
{X/Leandro,Y/joao}
• unif(conhece(joao,X),conhece(X,leandro) = fail
• unif(conhece(joao,X),conhece(Y,mae(Y)) =
{Y/joao, X/mae(joao)}
• unif(conhece(joão,X),conhece(Y,Z)) = {Y/João, X/Z}, ou
{Y/joão, X/Z, W/zelda} ou {Y/joão, X/joão, Z/joão} ...


Unificador mais geral: com menor número de variáveis
instanciadas
Substituição mínima: com menor número de pares Var/const
Revisão de L1: regra de resolução

simples:
(T  q )  ( p  r )  ( unif ( p , q )   )  ( ( r )  r ' )
 r'

ex.:
dog ( a )  ( dog ( X )  animal ( X ))
 animal ( a )

geral:
  X / a
( s1    s k  q1   q i   q l )
 ( p1   p j   p m  r1    rn )
 ( unif ( q i , p j )   )
 ( f  ( f )  f ' )
 (( s1 '  s k ' p1 ' p j 1 ' p j  1 '  p m ' )
 ( r1 '  rn ' q1 '  q i 1 ' q i  1 '  q l ' ))
Revisão de L1: demodulação

Unificação é uma operação puramente sintática:
• unif(P(a),P(b)) = fail mesmo se BC contém a = b
• necessidade de simplificar formulas depois da unificação
unificar para tomar em consideração igualdade semântica

Regra de demodulação:
t1  t 2
 f ( t 3  )
 unif ( t1 , t 3 )  
 f (  ( t 2 )  )

ex.:
(X  0  X )
 p ( X  Y ,Y * Z )
 p ( X ,0 * Z )
  Y / 0 
A curiosidade matou o gato? : em L1

Requisitos em inglês
1. Jack owns a dog.
2. Every dog owner is an animal
lover.
3. No animal lover kills an animal.
4. Either Jack or curiosity killed
Tuna
5. Tuna is a cat
0. Did curiosity kill the cat?

Em L1
1. x Dog(x)  Owns(Jack,x)
2. x (y Dog(y)  Owns(x,y)) 
AnimalLover(x)
3. x AnimalLover(x)  y
Animal(y)  Kills(x,y)
4. Kills(Jack, Tuna) 
Kills(Curiosity, Tuna)
5. Cat(Tuna)
6. x Cat(x)  Animal(x)
0. Kills(Curiosity,Tuna)
A curiosidade matou o gato? :
em forma normal

Em L1
1. x Dog(x)  Owns(Jack,x)
2. x (y Dog(y)  Owns(x,y)) 
AnimalLover(x)
3. x AnimalLover(x)  y
Animal(y)  Kills(x,y)
4. Kills(Jack, Tuna) 
Kills(Curiosity, Tuna)
5. Cat(Tuna)
6. x Cat(x)  Animal(x)
0. Kills(Curiosity,Tuna)

Em forma normal
1a. Dog(D)
1b. Owns(Jack, D)
2. Dog(y)  Owns(x,y)) 
AnimalLover(x)
3. AnimalLover(x)  Animal(y) 
Kills(x,y)  F
4. Kills(Jack, Tuna) 
Kills(Curiosity, Tuna)
5. Cat(Tuna)
6. Cat(x)  Animal(x)
0. Kills(Curiosity, Tuna)
A curiosidade matou o gato? :
exemplo de prova por refutação
Revisão de L1: estratégias de resolução
Refutação: aplicação repetitiva da regra de resolução
 Problema:

• a cada passo, como escolher o par de fórmulas a resolver?

Heurísticas:
• Resolver em prioridade formulas atómicas (unit
preference).
• Destacar um conjunto de formulas S (set of support) a
resolver em prioridade
• Sempre resolver uma formula inicial com uma formula
derivada (input resolution)
• Linear resolution (completa) = sempre escolher:


uma formula inicial com uma derivada qualquer
ou, 2 derivadas, uma sendo ancestral da outra