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 II • 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=HG R5=H H H┌┐G H┌┐G R7=(H └┘ G) H G H G R3=HG H G R6=(H ┌┐ G) H G R8=(HG) R9=(HG) 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.