Upload
harken
View
25
Download
2
Embed Size (px)
DESCRIPTION
Semântica de uma fórmula da lógica da 1 a ordem via modelo de Herbrand. Notação: const(F), func(F), pred(F), var(F) conjuntos de símbolos de constantes, funções, predicados e variáveis (respectivamente) de uma fórmula F da lógica da 1 a ordem Universo de Herbrand de F: - PowerPoint PPT Presentation
Citation preview
Semântica de uma fórmula da lógicada 1a ordem via modelo de Herbrand
Notação:Notação: const(F), func(F), pred(F), var(F) conjuntos de símbolos de constantes,
funções, predicados e variáveis (respectivamente) de uma fórmula F da lógica da 1a ordem
Universo de Herbrand de F:Universo de Herbrand de F: Uh(F) = const(F) {f(...,c,...) | f func(F) c const(F)}.
Base de Herband de F:Base de Herband de F: Bh(F) = Uh(F) {p(…,g,…) | p pred(F) g Uh(F)}.
Modelo de Herbrand de F:Modelo de Herbrand de F: Mh(F) = {q Bh(F) | F |= q}.
Modelo de Herbrand mínimo mínimo de F: mh é mínimo sse: mi Mh(F) mi mh
Menor Menor modelo mínimo de Herbrand de F: mm é o menor modelo mínimo sse: mi mi Mh(F) mm mi
Conjunto de proposicionalizações de F: groundground(F) = {F | substituição de var(F) por Uh(F)}
Negação por falha, raciocínio não monotônico e
semântica declarativa de programas lógicos
Jacques RobinCIn-UFPE
Modelo de Herbrand: exemplo
F:F: (maria = mae(joao) (X anc2(pai(X),X)) (Y anc2(mae(Y),Y)) (A,D anc2(A,pai(D)) anc2(A,D)) (E,F anc2(A,pai(D)) anc2(A,D))
Universo de Herbrand UUniverso de Herbrand Uhh(F):(F):
{maria, joao, mae(maria), mae(joao), mae(mae(maria)), mae(mae(joao)), ... }
Base de Herband BBase de Herband Bhh(F):(F):
{maria = joao, maria = mae(maria), maria = mae(joao), joao = mae(maria),
joao = mae(joao), ... anc(maria, maria), anc(maria,joao), anc(joao,maria), anc(joao,joao), anc(maria,mae(maria)), anc(mae(maria),maria)),
anc(maria,mae(joao)), ... } Modelo de Herbrand mínimo mModelo de Herbrand mínimo mhh(F): (F):
{maria = mae(joao), anc(maria,joao)}
Semântica declarativa de um programa lógico via formula da lógica da 1a ordem
Programa P:ancestor(A,D) :- parent(A,D).ancestor(A,D) :- parent(P,D), ancestor(A,P).
Semântica ingênua semIng(P): (A,D parent(A,D) ancestor(A,D))
(A,D,P parent(P,D) ancestor(A,P) ancestor(A,D))
Consultas C:?- ancestor(jacques,jacques)no
No entanto, em lógica clássica da 1a ordem: semIng(P) | C semIng não reflete semântica sobre hipótese do mundo fechadohipótese do mundo fechado Complementação de Clark comp(P): fórmula da lógica clássica da
1a ordem capturando semântica de P sobre hipótese do mundo fechado
Modelo de P = mh(comp(P))
Semântica declarativa de um programa lógico sobre hipótese do mundo fechado
Construção de comp(P):1.1. Para cada predicado definido por n regras C:- PPara cada predicado definido por n regras C:- P11. ,..., C:-P. ,..., C:-Pnn. substituir conjunção de implicações de semIng(P) por equivalência entre C, nas quais as variáveis U11,...,Ukk foram substituídas por novas variáveis V11,...Vkk,
e uma disjunção de n conjunções, cada uma da forma
...,Uii,... ... Vii = Uii ... Pmm(...,Uii,...).
2.2. Para cada predicado q(...,WPara cada predicado q(...,Wll,...) sem definição,...) sem definição como conclusão de nenhuma cláusula mas aparecendo em premissa de regra(s) definindo outro predicados
acrescentar fórmula Wl q(...,Wl,...)
Exemplo: P = {ancestor(A,D) :- parent(A,D). ancestor(A,D) :- parent(P,D), ancestor(A,P).} comp(P) = (Va,Vd ancestor(Va,Vd)
((A,D Va = A Vd = D parent(A,D)) (A,D,P Va = A Vd = D Vp = P parent(P,D) ancestor(A,P)))) P,C parent(P.C)
Em lógica da 1a ordem: comp(P) |= ancestor(jacques,jacques)
Negação por falha em programação em lógica
Programas lógicos normais ou geraisnormais ou gerais autorizam operador notnot de negação por falhanegação por falha nas premissaspremissas das regras e nas consultasconsultas.
Crucial notar que: not não é autorizado nem em fatos, nem em conclusão de regras Semanticamente, not é distinto da negação clássica negação clássica da lógica Enquanto uma premissa ou consulta S de uma BC em lógica é verdade sse: BC |= S
Uma premissa ou consulta not S de um programa lógico normal P é verdade sse: P | S
Negação por falha funciona com hipótese do mundo fechado Resolução SLD de Prolog estendida na resolução SLDNF
Raciocínio com negação por falha: inerentemente não monotônico
Adição de novos fatos em uma BC em Prolog com negação por falha pode diminuir, no lugar de aumentar, o número de fatos deriváveis
BC1:woman(X) :- human(X), not man(X).female(X) :- woman(X).human(roberta).?- female(roberta).yes. BC2 = BC1 + man(roberta).?- female(roberta).no.
Negação por falha e raciocínio por default
A não monotonicidade da negação por falha permite usá-la para implementar raciocínio por default
ave(piupiu). papaLeguas(bipbip). ave(X) :- papaLeguas(X). voa1(X) :- ave(X), not papaLeguas(X). voa2(X) :- not papaLeguas(X), ave(X). ?- voa1(X). X = piupiu. yes ; no ?- voa2(X). no. No entanto, Prolog ISO não segue uma semântica lógica
declarativa para a negação por falha
Negação por falhae terminação
man(X) :- human(X), not woman(X).
woman(X) :- human(X), not man(X). female(X) :- woman(X). human(roberta). ?- man(roberta). .......... Problema devido a recursão através da negação O conhecimento acima é fácil modelar pela re-introdução das restrições de integridade:false :- man(X), woman(X).woman(X) :- human(X).man(X) :- man(X).female(X) :- woman(X).human(roberta).
Limitações da semânticade complementação
P:P: edge(a,b). edge(c,d). edge(d,c). reachable(a).reachable(X) :- edge(Y,X), reachable(Y).sink(X) :- not edge(X,Y).?- reachable(c)...............?- sink(b).yes?- sink(X).no comp(P):comp(P): edge(a,b) edge(c,d) edge(d,c) (Vx reachable(Vx) (Vx = a Vx = X Y (edge(Y,X) reachable(Y)))) ((Vu sink(Vu) (Vu = U V
edge(V,U)))
Limitação 1:Limitação 1:comp(P) | reachable(c).comp(P) | reachable(d).
reachable(c)
(c=a Y(edge(Y,c) reachable(Y))
Y edge(Y,c) reachable(Y)
reachable(d) Limitação 2:Limitação 2:comp(P) | sink(b)
sink(b) (b=U V edge(V,U))
V edge(V,U) b=U
a
b
c
d
Semânticas declarativas para programas lógicos normais
Semântica de complementação de Clark válida apenas para programas lógicos definidosdefinidos, sem negação
Programa lógico estratificadoestratificado: sem ciclo de dependências entre predicados através de negação
Programa lógico consistenteconsistente: sem ciclo com número par de dependências entre predicados através de negação
Apenas programas lógicos normais estratificados possuem um único modelo mínimo de Herbrand definindo sua semântica
Programas lógicos normais mais gerais requerem outras semânticas
Extensões de Prolog ISO usam principalmente duas de tais semânticas: Semântica de modelos estáveismodelos estáveis (ou de conjunto de respostas)
Semântica bem fundamentadabem fundamentada
manhuman
woman
female
+
+ -
-
Semântica de programas lógicos normaisvia modelos estáveis
Objetivo de um modelo estável: definir conjunto de crenças consistentes para um agente racional
Rd(P,M) redução definida Rd de um programa lógico normal P com respeito a um modelo (ou hipótese) M: proposicionalização ground(P) menos:
as regras de P tendo como premissa a negação de um elemento de M as premissas negadas das regras restantes
Justificativa da redução: Na hipótese que L é verdadeverdade, regrasregras com not L em premissa não mudam o que pode ser deduzido e pode ser tirada sem mudar semântica de P
Na hipótese que L é falsofalso, premissaspremissas com not L não mudam o que pode ser deduzido e pode ser tirada sem mudar semântica de P
Resulta em um programa lógico definidodefinido pelo quais podem ser usada as semânticas de Herbrand e de Clark
M é um modelo estávelmodelo estável de um programa lógico normal P sse: M = mm(Rd(P,M)) Se é o menor modelo de Herbrand da redução de P com respeito a ele mesmo
Modelos estáveis de programas lógicos normais: exemplo
Programa P:man(X) :- human(X), not woman(X).woman(X) :- human(X), not man(X).female(X) :- woman(X).human(roberta). Proposicionalização ground(P).man(roberta) :- human(roberta), not woman(roberta).woman(roberta) :- human(roberta), not man(roberta).female(roberta) :- woman(roberta).human(roberta). Redução Rd(P, {human(roberta),man(roberta)}): man(roberta) :- human(roberta).female(roberta) :- woman(roberta).human(roberta). P tem 2 modelos estáveis mínimos:M1 = {human(roberta),man(roberta)}M2 = {human(roberta),woman(roberta),female(roberta)}
Modelos estáveis de programas lógicos normais: propriedades e limitações
Um programa lógico normal P é: CategóricoCategórico se possui um único modelo estável Inconsistente Inconsistente se possui nenhum
P é consistente e sem ciclos de dependência inteiramente positivo P tem pelo menos um modelo estável
Limitações dos modelos estáveis: dedução exponencial no tamanho da base fato alguns programas normais sem nenhum modelo estável
Exemplo: P= {a., b :- a. c :- not c}. Rd(P,{a,b}) = P que não tem menor modelo mínimo de Herbrand já que não é estratificado
Programação por conjuntos de respostas
Máquinas de inferência que usam: Programação em lógica, freqüentemente com várias extensões, como linguagem de representação do conhecimento
Proposicionalização e provadores de teoremas proposicionais para derivar modelos estáveis
Respostas as consultas diretamente lidas destes modelos
Interpretações ternárias de Herbrand
Lógica ternária: Interpretação ternária de Herbrand de uma fórmula F da lógica da 1a ordem I(F) = (I+,I-) onde I+: fatos supostos verdades da base de Herbrand de F, Bh(F)
I-: fatos supostos falsos da base de Herbrand de F, Bh(F)
I(F) total se I+ I- = Bh(F)
I(F) consistente se I+ I- = Ordem informacional entre
interpretações ternárias: I J sse I+ J+ e I- J-
Modelo de Herbrand ternário: M3(F) = ({q Bh(F) | F |= q}, {r Bh(F) | F |= r}).
P Q P Q PQ PQ PQ PQ
T
T F F T T T T
F F T F T F F
U F U U T F U
F
T T F F T T T
F T T F F T T
U T U F U T T
U
T U F U T T T
F U T F U F U
U U U U U T U
Semântica bem fundamentada de programas lógicos normais
R3(P,I) redução ternária R3 de um programa lógico normal P com respeito a uma interpretação de Herbrand ternária I: proposicionalização de P com cada premissa negada substituída pelo seu valor em I
M = WFM(P) é um modelo bem fundamentado de P sse: M = M3(R3(P,M))
Semântica bem fundamentada de programas lógicos normais: exemplo
Programa P:man(X) :- human(X), not woman(X).woman(X) :- human(X), not man(X).female(X) :- woman(X).human(roberta). Proposicionalização ground(P):man(roberta) :- human(roberta), not woman(roberta).woman(roberta) :- human(roberta), not man(roberta).female(roberta) :- woman(roberta).human(roberta). Redução R3(P, ({human(roberta)}, {})):
man(roberta) :- human(roberta), u.woman(roberta) :- human(roberta), u.female(roberta) :- woman(roberta).human(roberta). M = ({human(roberto)},{}) = M3(R3(P, M)) = WFM(P)
Semântica bem fundada: vantagens e limitações
Vantagens do modelo bem fundado: Dedução linear no tamanho da base de fato Todo programa normal tem um modelo bem fundado Exemplo:
P= {a., b :- a. c :- not c}. R3(P,({a,b},{})) = {a., b:- c., u :- not u}.
M3(R3(P,({a,b},{}))) = ({a,b},{}) = WFM(P).
Limitações do modelo bem fundado: Em alguns casos, deixa indefinidas valores que são deduzíveis a partir dos modelos estáveis
Exemplo: P: {p :- not q., q :- not p., r :- p., r :- q}. SM1(P) = {p, r}, SM2(P) = {q, r} WFM(P) = {{},{}}
Relações entre as várias semânticasde um programa lógico normal
Se P possui um único modelo estável SM(P) então: seu modelo bem fundado WFM(P) é total, e WFM(P) = SM(P)
Se P é estratificado então: S possui um único modelo estável SM(P) S possui um modelo bem fundado total WFM(P) SM(P) = WFM(P) = mm(comp(P)).