Raciocínio em Lógica de Descrições
Menandro Ribeiro Santana
Roteiro
 Introdução
 Raciocínio em DL
 Otimizações em Sistemas de Raciocínio
INTRODUÇÃO
Lógicas de Descrições
 Família de formalismos de representação do
conhecimento
Matemática.
baseados
na
Lógica
– Descrevem o domínio em termos de conceitos,
propriedades e indivíduos.
– Possuem semântica formal
– Provêem serviços de inferência.
Sintaxe e Semântica das DL’s
 Uma interpretação é um par <I, I>, onde:
– I é o universo de discurso (não-vazio)
– I é uma função de interpretação, que mapeia:
• Conceitos para subconjuntos de I
• Papéis para subconjuntos de II
• Instâncias para elementos de I
Sintaxe e Semântica das DL’s
Sintaxe e Semântica das DL’s
Famílias de DL’s
S = FL- +AL*+
papéis transitivos
– SHIQ
Base de Conhecimento em DL
 Par <TBox, ABox> onde:
– TBox (Terminological Box)
• Conhecimento Intensional: conhecimento
sobre o domínio do problema.
geral
– ABox (Assertional Box)
• Conhecimento Extensional: especifica um problema
particular.
TBox
 Conhecimento
intensional
na
forma
de
terminologia.
 Construído através de declarações que descrevem
as propriedades gerais dos conceitos.
– Conceito primitivo (base)
Pessoa
Fêmea
– Conceito complexo
Mulher ≡ Pessoa
┌┐
Fêmea
TBox
 As declarações do TBox são representadas como:
– Equivalências lógicas (condições necessárias e
suficientes) : ≡
– Inclusão (condições necessárias) : 
 Características das declarações:
– Somente é permitida uma definição para cada nome de
conceito.
– É recomendado que as definições sejam acíclicas, isto
é, não podem ser definidas em termos de:
• Elas mesmas
• Outros conceitos que indiretamente se referem a elas.
TBox - Exemplo
ABox
 Conhecimento extensional, que especifica
os indivíduos do domínio.
 Instanciação da estrutura de conceitos.
Tipos de Declarações no
ABox
 Declaração de Conceitos : C(a)
– Declara que “a” é um indivíduo do conceito C.
– Ex : Pessoa(Ana)
 Declaração de Papel : R(a,b)
– Declara que o indivíduo “a” está relacionado
com o indivíduo “b” através da propriedade R.
– Ex : temFilho(Ana,João)
ABox - Exemplo
RACIOCÍNIO EM DL
Raciocínio em DL
 Satisfatibilidade
 Subsunção
 Conseqüência Lógica
 Checagem de Equivalência
 Checagem de Consistência
 Checagem de Instância
 Consulta a Ontologia
Satisfatibilidade
 Um conceito é satisfatível com respeito a
um TBox T se existe uma interpretação I de
T tal que CI é não vazio. Neste caso
dizemos que I é um modelo de T.
Satisfatibilidade - Exemplo
TBox
 Mulher ≡ Pessoa ┌┐ Fêmea
 Mãe ≡ Mulher ┌┐  temFilho. Pessoa
Teste de Satisfatibilidade
 Mãe(a) ≡ Mulher(a) ┌┐ temFilho(a,b)
 Mãe(a) ≡ (Pessoa(a) ┌┐ Fêmea(a)) ┌┐ temFilho(a,b)
Insatisfatibilidade - Exemplo
TBox
 Mulher ≡ Pessoa ┌┐ Fêmea
 Homem ≡ Pessoa ┌┐ ¬Mulher
 Hermafrodita ≡ Homem ┌┐ Mulher
Teste de Satisfatibilidade
 Hermafrodita(a) ≡ Homem(a) ┌┐ Mulher(a)
 Hermafrodita(a) ≡ Pessoa(a) ┌┐ ¬Mulher(a) ┌┐
Mulher(a)
Subsunção
 Um conceito C é classificado por um
conceito D com respeito a um TBox T se CI
 DI para toda interpretação I de T. Neste
caso escrevemos C T D ou T ╞ C  D .
– O conceito D é chamado classificador
– O conceito C é chamado classificado.
Subsunção - Exemplo
TBox
 Mulher ≡ Pessoa ┌┐ Fêmea
 Mãe ≡ Mulher ┌┐  temFilho. Pessoa
Relacionamento entre os conceitos
 Mãe  Mulher
 Classificador : Mulher
 Classificado : Mãe
Conseqüência Lógica
 Se todo modelo da BC A é também modelo da
BC B, então B é Conseqüência Lógica de A
– TBox:
• teaches.Course  Undergrad └┘ Professor
– ABox:
• teaches ( john , cs415 ) ; Course ( cs415 ) ;
• Undergrad ( john )
– Professor ( john )?
Checagem de Equivalência
 Dois conceitos C e D são equivalentes com
respeito a um TBox T se CI = DI para toda
interpretação I de T. Neste caso escrevemos
C ≡T D ou T ╞ C ≡ D .
Checagem de Equivalência Exemplo
TBox
 Mulher ≡ Pessoa ┌┐ Fêmea
 Homem ≡ Pessoa ┌┐ ¬Mulher
 Masculino ≡ Pessoa ┌┐ ¬Fêmea





Expansão do TBox e Simplificação
Homem ≡ Pessoa ┌┐ ¬ Mulher
Homem ≡ Pessoa ┌┐ ¬(Pessoa ┌┐ Fêmea)
Homem ≡ Pessoa ┌┐ (¬Pessoa └┘ ¬Fêmea)
Homem ≡ (Pessoa ┌┐ ¬Pessoa) └┘ (Pessoa ┌┐ ¬Fêmea)
Homem ≡ Pessoa ┌┐ ¬Fêmea
Relacionamento entre os conceitos
 HomemI = MasculinoI
Checagem de Consistência
 Um ABox A é consistente com relação a
um TBox T se existe uma interpretação que
é modelo de ambos, A e T.
Checagem de Consistência Exemplo









TBox
Mulher ≡ Pessoa ┌┐ Fêmea
Homem ≡ Pessoa ┌┐ ¬Mulher
Pai ≡ Homem ┌┐  temFilho. Pessoa
ABox
Mulher(Jaguaraci)
Pai(Jaguaraci)
temFilho(Jaguaraci, Ana)
Mulher(Jaguaraci) ≡ Pessoa(Jaguaraci) ┌┐ Fêmea(Jaguaraci)
Pai(Jaguaraci) ≡ Homem(Jaguaraci) ┌┐ temFilho(Jaguaraci, Ana)
Homem(Jaguaraci) ≡ Pessoa(Jaguaraci) ┌┐ ¬Mulher(Jaguaraci)
Checagem de Instância
 Verifica se um dado indivíduo é uma
instância de um conceito específico.
 Exemplo:
TBox
Mulher ≡ Pessoa ┌┐ Fêmea
Mãe ≡ Mulher ┌┐  temFilho. Pessoa
ABox
Mulher(Maria)
temFilho(Maria,Pedro)
Checagem de Instância
Mãe(Maria)
Mãe(Maria) ≡ Mulher(Maria) ┌┐  temFilho. Pessoa
Consulta a Ontologia
 Encontra os indivíduos na base de
conhecimento que são instâncias de um
dado conceito.
 Exemplo:
ABox
Mulher(Maria)
Homem(João)
Homem(Pedro)
Resposta da Consulta
Homem → João, Pedro
Mulher → Maria
Redução
 É possível implementar os serviços de
raciocínio para o TBox a partir da
satisfatibilidade
ou
da
subsunção
dependendo da lógica de descrições
utilizada.
– Interseção (┌┐) e conceito de insatisfatibilidade
(┴) : Redução a Subsunção.
– Interseção (┌┐) e negação (¬) : Redução a
Satisfatibilidade.
Redução a Subsunção
 Proposição (Redução a Subsunção)
Para conceitos C e D temos:
(i) C é INSAT C  ┴ ;
(ii) C = D  (C  D) ┌┐ (D  C);
(iii) C e D disjuntos  (C ┌┐ D) 
┴ .;
Redução a Satisfatibilidade
 Proposição ( Redução a Satisfatibilidade )
Para conceitos C e D temos:
(i) C  D  (C ┌┐ ¬D)  ┴ .
(ii) C = D  (( C ┌┐ ¬D)  ┴) ┌┐ ((¬C ┌┐ D )  ┴);
(iii) C e D disjuntos  (C ┌┐ D)  ┴
Algoritmo Tableau
 Ao invés de testar diretamente a subsunção
dos conceitos, este algoritmo usa a negação
para
reduzir
a
subsunção
a
(in)satisfatibilidade dos conceitos.
C  D se somente se C ┌┐ ¬D é INSAT
Algoritmo Tableau
C  D se somente se (C ┌┐ ¬D) 
C  D ≡ C → D
 C → D ≡ ¬C└┘D
 Para realizar o
┴
algoritmo tableau é
necessário negar a expressão (¬C └┘ D) e
chegar a insatisfatibilidade.
 ¬(¬C └┘ D) ≡ C ┌┐ ¬D
 C ┌┐ ¬D é insatisfatível
Exemplo
 Sejam A e B nomes de conceitos e R o
nome de um papel. Analisar se (R.A)
(R.B) é subclasse de R.(A ┌┐ B).
 C = (R.A) ┌┐ (R.B) ┌┐ (¬ R.(A ┌┐ B))
 Forma normal de negação:
C0 = (R.A) ┌┐ (R.B) ┌┐ R.(¬A └┘ ¬B))
┌┐
 Construir uma interpretação finita I tal que
C0I  .
– Gerar um indivíduo b tal que b  C0I .
– b  (R.A)I, b  (R.B)I , b  R.(¬A └┘ ¬B)I.
– b  (R.A)I  deve existir um indivíduo c tal
que (b,c)  RI e c  AI .
– b  (R.B)I  deve existir um indivíduo d tal
que (b,d)  RI e d  BI .
–
–
–
–
b  R.(¬A └┘ ¬B)I.
c  (¬A └┘ ¬B)I e d  (¬A └┘ ¬B)I .
c  (¬A └┘ ¬B)I  c  (¬A)I ou c  (¬B)I .
d  (¬A └┘ ¬B)I  d  (¬A)I ou d  (¬B)I .
 Conclusão:
(R.A) ┌┐ (R.B) não é subclasse de R.(A ┌┐ B)
Algoritmo Tableau
 As
restrições são expressadas como
declarações do ABox.
 Seja C0 um conceito ALCN na forma de
negação normal.
 O algoritmo inicia com o ABox A0 = {C0(x0)}.
 Utilizar as Regras de transformação do
algoritmo de satisfatibilidade, até que
nenhuma delas possa ser usada.
 ABox Completo – ABox onde todos os ramos
possíveis foram expandidos.
Regras – Lógica Proposicional
R1=H ┌┐ G
H
G
R2=H └┘ G
R4=HG
R5=H
H
H┌┐G H┌┐G
R7=(H └┘ G)
H
G
H
G
R3=HG
H
G
R6=(H ┌┐ G)
H G
R8=(HG) R9=(HG)
H
G
H┌┐G H┌┐G
Regras – DL (ALC)
R1=(H ┌┐ G)(x)
H(x)
G(x)
R2=(H └┘ G)(x)
H(x)
G(x)
R3= (R.C)(x)
C(y)
onde y é um nome de indivíduo que não
R(x,y) ocorre em A
R4= (R.C)(x) e R(x,y)
C(y)
Regras – DL (N)
R6= (nR)(x)
R(x,z1)
R(x,z2)
:
R(x,zn)
R7= (nR)(x)
R(x,z1)
R(x,z2)
:
R(x, zn)
R(x, zn+1)
zi≠zj não está em KB (com i≠j)
zi=zj
Regras – DL (R+)
R8= (R.C)(x) e R+
C(y)
(R.C)(x) onde C não é atômico
Problema
- Regra gera recursividade
Solução
- Bloqueio, após perceber que nada de novo está
sendo gerado
Regras – DL (R+)
Regras – DL (R+)
Regras – DL (R+)
Algoritmo Tableau
 Um conceito C é insatisfatível sse
KB ┌┐ C = ┴ em todas as interpretações
– Cada ramo do Abox contém uma contradição
(clash) de um dos seguintes tipos:
1. {┴ (x)}  KB para algum nome de indivíduo x;
2. {A(x), ¬A(x)}  KB para algum nome de
indivíduo x e algum nome de conceito A;
3. (nR)(x)  R(x,yi) | 1  i  n+1}  {yi  yj | 1  i
 j  n+1}  KB para nomes de indivíduos x,
y1,..., yn+1 , um inteiro não negativo n e um nome
de papel R.
Aplicação do Tableau :
Exemplo 1
 Sejam A e B nomes de conceitos e R o
nome de um papel. Analisar se (R.A)
(R.B) é subclasse de R.(A ┌┐ B).
– C = (R.A) ┌┐ (R.B) ┌┐ (¬ R.(A ┌┐ B))
Forma normal de negação:
– C0 = (R.A) ┌┐ (R.B) ┌┐ R.(¬A └┘ ¬B))
┌┐
Aplicação do Tableau :
Exemplo 2
 Sejam A e B nomes de conceitos e R o nome
de um papel. Analisar se (R.A) ┌┐ (R.B)
 1 R é subclasse de R.(A ┌┐ B).
┌┐
– C = (R.A)┌┐(R.B)┌┐( 1 R)┌┐(¬ R.(A┌┐ B))
Forma normal de negação:
– C0 = (R.A)┌┐(R.B)┌┐( 1 R)┌┐R.(¬A└┘ ¬B))
Aplicação do Tableau :
Exemplo 3
 Seja a BC
– Conference  progChair.Person
– progChair.T  Event
– Conference (eswc)
 Provar
– Event(eswc)
– Verificar se Conference (eswc) ┌┐ ¬Event(eswc)
é insatisfatível
Aplicação do Tableau :
Exemplo 3
OTIMIZAÇÕES EM SISTEMAS
DE RACIOCÍNIO
Expansão do TBox - Unfold
 Pode-se reduzir os problemas de raciocínio
com relação a um TBox acíclico T para
problemas com respeito ao TBox vazio.
– TBox vazio: TBox no qual todos os conceitos
complexos são definidos apenas com a
utilização de conceitos primitivos.
– Necessário expandir as definições de conceitos
armazenados no TBox.
– Permite encontrar mais facilmente as
semelhanças entre conceitos, contradições, etc.
Expansão do TBox
 Cada definição está na forma A ≡ D onde D
contém somente símbolos base.
– OBS: A  D pode ser substituído por A ≡ Ā ┌┐
D , sendo que Ā é um novo símbolo base.
 Para cada conceito C, definimos a expansão
de C com respeito a T como o conceito C’
que é obtido de C pela substituição de cada
ocorrência de um nome de símbolo A em C
pelo conceito D.
Expansão do TBox - Exemplo
 Mulher ≡ Pessoa
┌┐
Fêmea
 Homem ≡ Pessoa ┌┐ ¬Mulher
 Mãe ≡ Mulher ┌┐  temFilho. Pessoa
 Pai ≡ Homem ┌┐  temFilho. Pessoa
 Pais ≡ Pai └┘ Mãe
Expansão do TBox - Exemplo
 Mulher ≡ Pessoa ┌┐ Fêmea
 Homem ≡ Pessoa ┌┐ ¬ (Pessoa ┌┐ Fêmea)
 Mãe ≡ (Pessoa ┌┐ Fêmea) ┌┐  temFilho.
Pessoa
 Pai ≡ (Pessoa ┌┐ ¬ (Pessoa ┌┐ Fêmea)) ┌┐
 temFilho. Pessoa
 Pais ≡ ((Pessoa ┌┐ ¬ (Pessoa ┌┐ Fêmea))
┌┐  temFilho. Pessoa)
┌┐
((Pessoa
└┘
Fêmea) ┌┐  temFilho. Pessoa)
Otimizações de préprocessamento
 Normalização
 Absorção
Normalização
 Simplificação da BC identificando :
– Equivalências sintáticas
– Contradições e
– Tautologias
 Todos os conceitos devem ser modificados
para se adequar a um formato padrão
– Utiliza apenas o conjunto completo de
conectivos ¬ e ┌┐.
Normalização
 Exemplos:
(¬D └┘ ¬C) é transformado em ¬(D ┌┐ C).
∃ R.⊥ é simplificado para ⊥.
Absorção
 Eliminação de axiomas gerais aumentando a
definição destes axiomas.
– Axiomas gerais na forma C ⊆ D,
• C é um conceito não atômico
• São manipulados até chegar em A ⊆ D’, onde A é
atômico.
– Este axioma pode então ser fundido dentro de
uma definição primitiva existente A ⊆ C’, para
resultar em A ⊆ C’ ┌┐ D’.
Regras de Absorção
 A ┌┐ B ⊆ D, A atômico
A ⊆ D └┘ ¬ B.
 A └┘ B ⊆ D, A atômico
A ⊆ D ┌┐ ¬ B.
Absorção
 Exemplo:
(Homem ┌┐ ∃ temFilho.Pessoa ⊆ Pai) resulta em
(Homem ⊆ Pai └┘ ¬∃ temFilho.Pessoa)
Homem ⊆ ¬ Mulher
Absorção:
Homem ⊆ ¬ Mulher ┌┐ (Pai └┘ ¬∃ temFilho.Pessoa)
Otimizações de Classificação
 Hierarquia de conceitos representada por
um grafo acíclico direto
– Nós são rotulados com os nomes dos conceitos
– Arcos correspondem a relações de classificação
 Um conceito A classifica um conceito B se:
– Ambos A e B estão no rótulo do mesmo nó x
– A está no rótulo de algum nó x, e existe um
arco (x,y) no grafo e um conceito (s) no rótulo
do nó y, que classifica B.
Otimizações de Classificação
 Hierarquia de conceitos representada por
um grafo acíclico direto
– Nós são rotulados com os nomes dos conceitos
– Arcos correspondem a relações de classificação
 Um conceito A classifica um conceito B se:
– Ambos A e B estão no rótulo do mesmo nó x
– A está no rótulo de algum nó x, e existe um
arco (x,y) no grafo e um conceito (s) no rótulo
do nó y, que classifica B.
Otimizações de Classificação
 Minimização do número de testes de
classificação através de algoritmos de busca
que percorrem o grafo:
– Da base para o topo: encontra conceitos
classificados
– Do topo para a base: encontra conceitos
classificadores.
 São encontradas as classificações óbvias,
diminuindo o custo de processamento
causado pelo teste de classificação.
Otimizações de Classificação
 Transitividade da relação de subsunção:
– Se A não é subclasse de B, então ele não pode
ser subclasse de nenhum outro conceito que seja
subclasse de B.
• Busca do topo: testa se A classifica B somente
quando se sabe que B é subclasse de todos os
conceitos que classificam A.
• Busca da base: testa se A classifica B somente
quando se sabe que A classifica todos os conceitos
que são subclasse de B.
Otimizações do Teste de
Subsunção
 Detecta não-classificações óbvias.
 Baseia-se no armazenamento das árvores de
expansão construídas anteriormente para
evitar repetições futuras.
 Exemplo:
A ≡ C ┌┐ R1C1 ┌┐ R2C2
B ≡ ¬D └┘ R3C3.
Provar que A não é subclasse de B
A┌┐¬B é satisfatível
Otimizações do Teste de
Subsunção
Otimizações do Teste de
Satisfatibilidade
 Teste realizado após a execução de todas as
otimizações.
– Diminuição de custo computacional.
 Algoritmo Tableau
– Padrão: Ramos Sintáticos
– Otimizado: Ramos Semânticos
Ramos Semânticos
 Ramos sintáticos
– Ao expandir um nó do grafo (árvore), escolhese uma disjunção não expandida e inicia-se a
busca pelos diferentes modelos gerados pela
adição de cada um dos membros da disjunção.
– Não há uma prevenção de recorrência de um
conceito insatisfatível em ramos diferentes.
– Alto custo dependendo da dificuldade
encontrada para provar a insatisfatibilidade
deste conceito disjunto.
Ramos Semânticos
 Ramos semânticos:
– Ao expandir um nó do grafo (árvore), escolhese um dos membros isolados da disjunção não
expandida e gerasse dois novos ramos,
adicionando em um ramo o conceito escolhido
e no outro a sua negação.
– Não ocorrem buscas desnecessárias como na
busca por ramos sintáticos, pois os ramos são
estritamente disjuntos.
Ramos Semânticos
Busca Sintática de Ramos
Busca Semântica de Ramos
Bibliografia
 NARDI, D.; BRACHMAN, R. “An Introduction to Description
Logics”. In: The Description Logic Handbook – Theory,
Implementation and Applications. Editedy by Franz Baader, Diego
Calvanese, Deborah McGuinness, Daniele Nardi and Peter PatelSchneider, 2003.
 BAADER, F.; NUTT, W. “Basic Description Logics”. In: The
Description Logic Handbook – Theory, Implementation and
Applications. Editedy by Franz Baader, Diego Calvanese, Deborah
McGuinness, Daniele Nardi and Peter Patel-Schneider, 2003.
 BAADER, F. “Description Logic Terminology”. In: The Description
Logic Handbook – Theory, Implementation and Applications. Editedy
by Franz Baader, Diego Calvanese, Deborah McGuinness, Daniele
Nardi and Peter Patel-Schneider, 2003.
Bibliografia
 HORROCKS, I. “Implementation and Optimisation Techniques”. In:
The Description Logic Handbook – Theory, Implementation and
Applications. Editedy by Franz Baader, Diego Calvanese, Deborah
McGuinness, Daniele Nardi and Peter Patel-Schneider, 2003a.
 VIEIRA, R.; ABDALLA, D.; SILVA, D. M.; SANTANA, M. R. “Web
Semântica: Ontologias, Lógicas de Descrições e Inferências”. In:
Web e Multimídia: Desafios e Soluções. PUC Minas, 2005.
Download

[Nome da empresa]