Programação em lógica e lógicaProgramação em lógica e lógica

Jacques Robin, DI-UFPEwww.di.ufpe.br/~jr

O que é Prolog?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ógicaMetá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 PLLinguagens 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 mundoPL 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 Ciclo de desenvolvimento de um software baseado em conhecimentosoftware baseado em conhecimento

AQUISIÇÃO

FORMALIZAÇÃO

IMPLEMENTAÇÃO

MANUTENÇÃO

Nível de Conhecimento

Nível Lógico

Ontologia

Raciocínio

Nível de Implementação BASE

Raciocínio automático em software Raciocínio automático em software baseado em conhecimentobaseado em conhecimento

Propriedades desejáveis:• correto: • completo: • composicional:

)))'(|)(()'|((', RsemRsemRRRR ))'|())'(|)(((', RRRsemRsemRR

)))))(,),(()(((

)),,((((,,

1

11

N

NN

RsemRsemgRsemg

RRfRfRRR

Programação procedimental Programação procedimental x programação declarativax 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 L1 como FRC e linguagem de programação declarativa: motivaçãoprogramaçã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: sintaxeRevisão de L1: sintaxeFó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 Wumpus | Agente | Flecha | ...Variável x | y | wumpus | agente | ...Predicado Adjacente | Vivo | ...Função Em | Brisa | ...

Revisão de L1: semânticaRevisã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 Revisão de L1: mecanismo de inferência completo (para inferência completo (para

verificaçãoverificação))

Fórmula da lógica de 1a. ordem

Fórmula na forma normal

Fórmula instanciada ou False

Conversão para forma normal

Prova por Refutação

Resolução Unificação Demodulação

Revisão de L1:Revisão de L1:forma normal (1)forma normal (1)

Def:

Thm: Regras de conversão:

• implicação:• negação:

• variáveis:

FNLNLF I ,1,1

atómicasformulassãoppjionde

ccppNLNL

ji

mnI

,,

/ 1111

)()( qpqp

pp

XpXXpX

XpXXpX

qpqp

qpqp

)(

))(,()))(,((

))(,()))(,((

)())((

)())((

)))(())((()))(())((( YqYXpXXqXXpX

Revisão de L1:Revisão de L1:formal normal (2)formal normal (2)

Regras de conversão (cont.):• quantificadores:• skolemização:

• distributividade:• associatividade:

• disjunções:

Quantificação universal implícita

)))()((()))(()(( XqYpXXqXYp

))),((())(,(

)())((

aYfpYXpXY

apXpX

))()(())(( rqrprqp

)())(())((

)())(())((

rqprqprqp

rqprqprqp

))()(()( rqsprqsp

Revisão de L1: refutação, Revisão de L1: refutação, unificação e substituiçãounificaçã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 posicionalRevisã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çãoRevisão de L1: regra de resolução

simples:

ex.:

geral:

'

)')(()),(()()(

r

rrqpunifrpqT

))''''''(

)''''''((

)')((

)),((

)(

)(

1111

1111

11

11

liin

mjjk

ji

nmj

lik

qqqqrr

ppppss

fff

pqunif

rrppp

qqqss

aXaanimal

XanimalXdogadog/

)(

))()(()(

Revisão de L1: demodulaçãoRevisã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:

ex.:

))((

),(

)(

2

31

3

21

tf

ttunif

tf

tt

0/

)*0,(

)*,(

)0(

Y

ZXp

ZYYXp

XX

A curiosidade matou o gato? A curiosidade matou o gato? : em L1: 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

Tuna5. Tuna is a cat0. 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? A curiosidade matou o gato? ::em forma normalem forma normal

Em L11. 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) F4. Kills(Jack, Tuna)

Kills(Curiosity, Tuna)5. Cat(Tuna)6. Cat(x) Animal(x)0. Kills(Curiosity, Tuna)

A curiosidade matou o gato? A curiosidade matou o gato? ::exemplo de prova por refutaçãoexemplo de prova por refutação

Revisão de L1: estratégias de Revisão de L1: estratégias de resoluçãoresoluçã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