Trabalho de Graduação: Normalização de ontologias em lógica de descrições para o raciocínio com o provador de teoremas leanCoP

Universidade Federal de PernambucoCentro de Informática

Graduação em Ciência da Computação

Normalização de ontologias em lógica dedescrições para o raciocínio com o

provador de teoremas leanCoP

Adriano Silva Tavares de Melo

Trabalho de Graduação

Recife11 de julho de 2011

Universidade Federal de PernambucoCentro de Informática

Adriano Silva Tavares de Melo

Normalização de ontologias em lógica de descrições para oraciocínio com o provador de teoremas leanCoP

Trabalho apresentado ao Programa de Graduação em Ci-ência da Computação do Centro de Informática da Univer-sidade Federal de Pernambuco como requisito parcial paraobtenção do grau de Bacharel em Ciência da Computação.

Orientador: Fred Freitas

Recife11 de julho de 2011

Eu dedico este trabalho a Alcimary Silva, tia querida quenão está mais entre nós.

Agradecimentos

Gostaria de agradecer à minha mãe, que sempre acreditou em mim, que me deu condições deestudar, que abdicou de várias coisas ao decorrer de sua vida para dar prioridade aos filhos, quenos incentivou a crescer, que nos ensinou valores, que, em fim, nos amou incondicionalmente.

Agradeço a todos da minha família que me apoiaram a estudar e a trilhar caminhos que medeixaram longe, em especial ao meu irmão, madrinha e avó, que sempre me falam o quanto sãoorgulhosos da minha decisão de sair da minha cidade para evoluir profissionalmente. Obrigado!

Agradeço à minha namorada, que tornou essa jornada longe dos amigos e família maisagradável e feliz.

Agradeço a Fred, que sempre que precisei se mostrou disposto a ajudar e que me ensinoumuito nos últimos anos.

Agradeço a todos que me ajudaram profissionalmente e academicamente, eu não teria con-seguido chegar até aqui sem essa ajuda. Obrigado!

iv

Uma vida de sacrifício é o cume supremo da arte; é cheia de alegriaverdadeira.

—MOHANDAS KARAMCHAND GANDHI

Resumo

A Web Semântica promete revolucionar o jeito de como as pessoas interagem na Web. Osconceitos de agentes inteligentes, serviços baseados em semântica de documentos e empresasse comunicando com empresas através de agentes baseados em regras deverão ser abundantesnesse novo cenário.

Várias tecnologias estão sendo estudadas e construídas para formar uma nova infra-estruturapara a Web. Entre elas estão os elementos que formarão a camada de lógica e prova, contextoque está inserido este trabalho.

Este trabalho propôe implementar parte do algoritmo do método das conexões para lógicade descrição, usado para fazer atividades de raciocínio em uma base de conhecimento. Omódulo a ser implementado é a conversão dos axiomas da base de conhecimento para a formanormal positiva.

Palavras-chave: método das conexões, lógica de descrição, lógica, inteligencia artificial

vi

Abstract

The Semantic Web promises to revolutionize the way people interact on the Web. Conceptslike intelligent agents, semantic-based services, business-to-business communication betweencompanies through rule-based agents should be plentiful in this new scenario.

Several technologies are being studied and constructed to form a new infrastructure for theWeb. These are the elements that form the layer of logic and proof, context that this project isinserted.

This project proposes to implement part of the algorithm of the connection method fordescription logic, used to do activities of reasoning in a knowledge base. The module to beimplemented is the conversion of the axioms of the knowledge base for the positive normalform.

Keywords: connection method, description logic, artificial intelligence

vii

Sumário

1 Introdução 11.1 Web Semântica 1

1.1.1 Aplicações 21.1.1.1 Gerenciamento de Conhecimento 21.1.1.2 Comércio eletrônico Business to Consumer (B2C) 21.1.1.3 Comércio eletrônico Business to Business (B2B) e agentes

pessoais 31.1.2 Tecnologias 3

1.1.2.1 Metadados Explícitos 31.1.2.2 Ontologias 41.1.2.3 Lógica 51.1.2.4 Agentes 5

1.2 Organização da Monografia 5

2 Lógica de Descrição ALC 62.1 Sintaxe da Lógica de Descrição 62.2 OWL: Web Ontology Language 7

2.2.1 OWL Full 82.2.2 OWL DL 92.2.3 OWL Lite 9

3 Normalização para o método das conexões 103.1 Tradução de ontologias ALC para forma normal disjuntiva 10

3.1.1 Algoritmo Proposto 123.1.2 Algoritmo Original 18

4 leanCoP 22

5 Conclusão e trabalhos futuros 245.1 Conclusão 245.2 Trabalhos futuros 24

viii

Lista de Figuras

1.1 Código HTML de uma página da americanas.com 41.2 Exemplo de código com semântica para um produto 4

3.1 Método Normalize-Ontology () 193.2 Método Normalize-LHS () 193.3 Método Normalize-RHS () 20

ix

Lista de Tabelas

2.1 Notação da lógica de descrição 72.2 Sintaxe e semântica de alguns contructos de lógica de descrição com anotação

de expressividade 8

x

CAPÍTULO 1

Introdução

A World Wide Web é uma das tecnologias mais revolucionárias que o homem já inventou. Elamudou em escala global a forma com que pessoas e empresas trocam informações, contribuindopara que o conhecimento se tornasse mais universal e que limites físicos e lingüísticos fossemcada vez mais minimizados.

A web como conhecemos hoje nasceu de uma proposta feita por Tim Berners-Lee à em-presa CERN em 1989 [BL89]. O problema enfrentado pela empresa na época era a perca deinformações internas por falta de documentação ou pela saída de algum funcionário. A soluçãoproposta por Berners-Lee foi fazer uma rede de documentos interligados por hyperlinks em quecada setor da empresa poderia adicionar novos documentos.

A estrutura básica que Berners-Lee montou a 22 anos evoluiu a passos largos em relaçãoà escalabilidade e padronização de protocolos e linguagens, tendo hoje cerca de 2 bilhões deusuários, mais de 30% da população do planeta.

Apesar do avanço das infra-estruturas e serviços para a Web, ainda há muito o que evoluir.Uma das propostas de mudanças é prover uma maior expressividade da linguagem que des-creve os documentos na Web [Hef04]. Hoje, esses documentos não possuem um significadoque possa ser extraído de forma concisa, apresentam ambigüidade, misturam os dados comelementos visuais e muitas vezes não podem ser indexados por engenhos de busca.

1.1 Web Semântica

"I have a dream for the Web [in which computers] become capable of analyzingall the data on the Web, the content, links, and transactions between people andcomputers. A Semantic Web which should make this possible has yet to emerge, butwhen it does, the day-to-day mechanisms of trade, bureaucracy and our daily liveswill be handled by machines talking to machines. The intelligent agents peoplehave touted for ages will finally materialize."Tim Berners-Lee

Tradução literal: "Eu tenho um sonho para a Web [em que os computadores]tornam-se capazes de analisar todos os dados na Web, o conteúdo, links, e astransações entre pessoas e computadores. A Web Semântica que deve tornar issopossível ainda está para surgir, mas quando isso acontecer, os mecanismos dia-a-dia da burocracia do comércio e nossas vidas diárias serão tratados por máquinasfalando com máquinas. Os agentes inteligentes que as pessoas têm falado poranos vão finalmente se concretizar."Tim Berners-Lee

1

1.1 WEB SEMÂNTICA 2

A Web Semântica citada no texto de Berners-Lee acima é uma iniciativa de pesquisadoresda área de inteligência artificial e lingüística computacional que estudam como adequar a Webde hoje a uma infra-estrutura que a tornará mais acessível às máquinas. Essa nova roupagemque os pesquisadores querem dar à Web permitirá que serviços mais sofisticados possam serconstruídos, como os que serão descritos a seguir.

1.1.1 Aplicações

1.1.1.1 Gerenciamento de Conhecimento

Gerenciamento de conhecimento está relacionado à aquisição, acesso e manutenção de conheci-mento dentro de uma empresa ou organização. Essa atividade se tornou e está se estabelecendocomo uma necessidade básica em grandes empresas visto que o conhecimento que é gerado in-ternamente agrega valor, pode se tornar um diferencial competitivo e também pode aumentar aprodutividade de seus colaboradores. Com o uso de tecnologias criadas para a Web Semântica,soluções para G.C. podem melhorar em vários aspectos, entre eles:

• Organização do conhecimento existente a partir de seu significado;

• Geração de novas informações de forma automática;

• Checagem de inconsistências semânticas em documentos;

• Substituição de consultas baseadas em palavras-chave por perguntas em linguagem na-tural;

1.1.1.2 Comércio eletrônico Business to Consumer (B2C)

O comércio eletrônico entre vendedores e consumidores é um dos modelos de negócio na Inter-net que melhor se estabeleceu, sites como amazon 1, americanas 2 e mercado livre 3 possuempúblico fiel e que os visitam por vários objetivos. É muito comum para a geração que cresceuimersa na Web entrar em sites de compra como esses a procura do melhor preço antes de de-cidir fazer uma compra. Muitas vezes o produto não é adquirido em uma loja virtual, mas apesquisa inicial de preços é que muitas vezes determina a escolha do produto. Observando essecomportamento, sites como o buscapé 4 fazem o trabalho de indicar qual é a loja que está como melhor preço.

A Web Semântica pode ajudar nesse cenário provendo interfaces de consulta mais com-pletas aos sites que fazem comparação de preços, porém, com muito mais detalhes técnicossobre o produto. Supondo que cada produto tem, por exemplo, uma ontologia que o descreveem detalhes (provida pelo fabricante ou por sites de review de produtos), o consumidor poderáfazer comparações muito mais detalhadas, ajudando-o a encontrar o produto que vai suprir asua necessidade.

1site: amazon.com2site: americanas.com3site: mercadolivre.com.br4site: buscape.com.br


1.1.1.3 Comércio eletrônico Business to Business (B2B) e agentes pessoais

A maioria das pessoas que compram serviços ou produtos na Web só conhecem o comércioeletrônico do tipo B2C, mas existem tecnologias para comércio do tipo B2B, Business to Bu-siness, agentes computacionais de empresas que se comunicam para fechar acordos e otimizaro ciclo de negócios que muitas vezes já podem ser previstos e modelados.

Com a popularização da Web Semântica e a introdução de agentes pessoais e agentes querepresentam negócios, eles poderão se comunicar de forma mais natural e aplicações para oti-mizar tarefas do dia-a-dia que poderão ser produzidos. Por exemplo, um médico que possuaum agente pessoal que negocie a sua agenda com os agentes pessoais de seus clientes pode serutilizado para remarcar seus atendimentos em caso de uma viagem ou imprevisto, agindo comouma secretária virtual.

1.1.2 Tecnologias

Aplicações como as citadas acima já existem, mas o trabalho de engenharia para conseguirbons resultados é alto devido às tecnologias que são adotadas hoje. Vamos usar o case do sitede comparação de preços BuscaPé na próxima seção da monografia.

1.1.2.1 Metadados Explícitos

A primeira tarefa de engenharia de um agente coletor de preço, como os do buscaPé, é fazê-lovisitar vários sites de compras todo dia à procura de modificações nas listas de produtos parasaber quais estão disponíveis naquela loja. É feito então o parsing do HTML de cada site decompras à procura das informações de preço, descrição, avaliação e detalhes de cada produto. Alimitação dessa abordagem é que sempre que um dos sites de compra mudar o layout (estruturado HTML), um novo script de parsing deverá ser escrito. A grande demanda técnica de umaaplicação como essa é a escrita de agentes muito especializados para atingir bons resultados.

Na figura 1.1 está parte do código em HTML de uma página de produtos da america-nas.com. As informações do produto estão cercados apenas de código para a renderização dessapágina pelo navegador. Ou seja, a única preocupação dos engenheiros da americanas.com foi aleitura por humanos da informação do produto. Uma aplicação que deseje usar as informaçõesdos produtos da loja vai ter que fazer um agente especializado no parsing desse código.

Motores de busca que também se baseiam em parsing de páginas para extrair informaçõesda Web dificilmente saberão, por exemplo, qual é o preço de um produto nesse site da ame-ricanas.com, já que há várias informações de preço na página e o parsing que é feito não éotimizado para sites específicos.

A conseqüência para o usuário final é que ele terá que usar um site específico como obuscapé ou terá que fazer buscas a um engenho de busca por palavras-chave para achar ossites de compra que possuam um produto e em uma segunda etapa, fazer a análise de preçosmanualmente.

A abordagem da Web Semântica para resolver problemas como esse não é fazer agentesespecializados (como os do buscapé), e sim, anotar metadados semânticos dos documentosdisponíveis na Web. O exemplo dado anteriormente seria escrito na figura 1.2.


Figura 1.1 Código HTML de uma página da americanas.com

Figura 1.2 Exemplo de código com semântica para um produto

1.1.2.2 Ontologias

O termo ontologia vem da filosofia, nesse contexto, é um ramo da filosofia que se dedica aestudar a natureza da existência, concentra-se em identificar e descrever o qu existe no universo.Em computação, uma ontologia é um artefado para descrever um domínio. Consiste em umalista finita de termos e relações entre eles. Os termos denotam conceitos importantes de umdomínio [AH08].

Grande parte dos trabalhos referentes à Web Semantica estão ligados a ontologias, inclusiveeste. As linguagem de descrição de ontologias mais importântes para a Web são:

• XML: usado para dirigir a sintaxe de documentos estruturados. Não impôe restriçõessemânticas no conteúdo do documento;

• XML Schema: linguagem para impor restrições na estrutura dos documentos XML;

• RDF: modelo de dados para recursos (objetos) e relações entre eles. As restrições se-mânticas são fixas e podem ser representados a partir da sintaxe do XML;

• RDF Schema: descreve as propriedades e classes dos objetos RDF;

• OWL: linguagem rica para modelagem de classes, propriedades, relações entre classes(e.g. disjunção), restrições de cardinalidade, características de propriedades (e.g. sime-tria). Mais detalhes sobre a OWL serão dados no capítulo 2 dessa monografia.

1.2 ORGANIZAÇÃO DA MONOGRAFIA 5

1.1.2.3 Lógica

Lógica é a disciplina que estuda os princípios do raciocínio. Ela provê linguagens formais paraexpressar conhecimento, a semântica formal para a interpretação de sentenças sem precisarrealizar operações sobre a base de conhecimento e a transformação de conhecimento implícitoem conhecimento explícito, através de deduções a partir da base de conhecimento [AH08].

Lógica é mais geral que ontologias, ela pode ser usada por agentes inteligentes para tomadade decisões e escolha de ações. Por exemplo, um agente de B2C pode dar um desconto a umcliente baseado na seguinte regra:

∀x∀y,cliente(x)∧ produto(y)∧ clienteFiel(x)→ desconto(x,y,5%)

Onde cliente(x) indica que x é um cliente/consumidor, produto(y) indica que y é um produtode uma loja, clienteFiel(x) indica que x é um cliente fiel da loja e desconto(x, y, 5%) indica queo cliente x terá um desconto de 5% no produto y.

1.1.2.4 Agentes

Um agente é tudo o que pode ser considerado capaz de perceber seu ambiente por meio desensores e de agir sobre esse ambiente por meio de atuadores [RN02]. Agentes lógicos sãoaqueles que executam ações através de uma base de conhecimento e possuem um requisitofundamental, quando ele formula uma pergunta para a base de conhecimento, a resposta deveseguir o que já foi informado anteriormente.

Agentes para a Web Semântica utilizam as três tecnologias que já foram descritas:

• Metadados serão usados para identificar e extrair informações da Web;

• Ontologias serão usadas para dar assistência às consultas realizadas à Web, interpretarinformações recuperadas e para comunicação com outros agentes;

• Lógica será usada para processar informações recuperadas, chegar a conclusões e tomardecisões;

1.2 Organização da Monografia

Esta monografia está dividida em cinco capítulos. No Capítulo 1, é apresentada uma visãogeral sobre a Web Semântica, exemplificando com aplicações e citando as tecnologias que estãosendo usadas. No Capítulo 2, são apresentados conceitos referentes a Lógica de Descrição ea sua ligação com a linguagem de descrição de ontologias OWL. No Capítulo 3 são descritosos algoritmos para normalização de ontologias para a Forma Normal Positiva. No Capítulo 4 oLeanCop é apresentado e é mostrada a validação do trabalho realizado. O Capítulo 5 apresentaas considerações finais sobre o trabalho, bem como propostas de trabalhos futuros.

CAPÍTULO 2

Lógica de Descrição ALC

Lógica de Descrição é uma família de linguagens de representação de conhecimento que podeser usada para representar o conhecimento de domínio de uma aplicação de forma estruturadae formal [BCM+03].

A motivação para estudar lógica de descrição neste trabalho vem da Web Semântica. Paraque as máquinas possam fazer inferências sobre os documentos da Web, é preciso que a lin-guagem de descrição dos documentos vá além da semântica básica definida pelo RDF Schemae consiga definir e descrever classes e propriedades sobre os objetos encontrados na Web.

2.1 Sintaxe da Lógica de Descrição

Nessa seção será mostrada a sintaxe básica da lógica de descrição. A tabela 2.1 mostra oalfabeto de símbolos usado pela linguagem.

Os elementos mais básicos são os conceitos atômicos e propriedades atômicas. Descriçõesde conceitos podem ser construídas indutivamente a partir dos construtores com conceitos epropriedades.

C,D→ A | (conceito atômico)> | (conceito universal)⊥ | (conceito vazio)¬A | (negação de conceito atômico)CuD | (interseção de conceitos)∀R.C | (restrição de valor)∃R.> (restrição existencial)

Uma interpretação ι consiste em um conjunto não vazio ∆ι (domínio da interpretação) euma função de interpretação, que para conceito atômico A é o conjunto Aι ⊆ ∆ι e para cadapropriedade atômica R é a relação binária Rι ⊆ ∆ι ×∆ι . As funções de interpretação se esten-dem a descrição de conceitos a partir das definições indutivas [BCM+03] como as que estãoabaixo:

>ι = ∆ι

⊥ι = /0¬Aι = ∆ι\Aι

(CuD)ι = Cι ∩Dι

(∀R.C)ι = {a ∈ ∆ι |∀b.(a,b) ∈ Rι → b ∈Cι}(∃R.>)ι = {a ∈ ∆ι |∃b.(a,b) ∈ Rι}

6

2.2 OWL: WEB ONTOLOGY LANGUAGE 7

alfabetoa, b indivíduosA, B conceitos atômicosC, D descrição de conceitosR, S papeis (propriedades)f, g símbolos de funções

conectivosu interseçãot união¬ negação

relaçõesv inclusão≡ equivalência

Tabela 2.1 Notação da lógica de descrição

Esse trabalho é restrito à família ALC, que compreende os conceitos e propriedades atômi-cas, negação de conceitos, interseção, união, restrições de valor e existencial, top (verdade)e bottom (absurdo). A tabela 2.2 mostra além de ALC, outras famílias de DL existentes[BCM+03].

Uma ontologia ou base de conhecimento em ALC é composta pela tripla (NC,NR,NO), ondeNC é o conjunto de conceitos, NR é o conjunto de predicados, e NO é o conjunto de indivíduos,que são as instâncias de NC e NR. A base de conhecimento ou ontologia também pode serdescrita como o par (τ,α), onde τ é a terminologia do domínio (TBox), equivalente a NC∪NCe α é a instanciação da base, que corresponde a NO, também conhecida como assertional box(ABox).

Os axiomas são compostos por elementos de NO e um conjunto finito de GCIs (generalconcept inclusions). Podem assumir a forma C v D ou C ≡ D (uma equivalência (≡) é omesmo que (C v D)∧ (DvC) ), onde C,D são conceitos e v é uma inclusão.

2.2 OWL: Web Ontology Language

A Web Ontology Language, OWL, foi escolhida pela w3c 1, grupo que regula os padrões naWeb, como a linguagem de descrição de ontologias para a Web Semântica [Hef04]. Algunsdos requisitos que ela atendeu foram [AH08]: i) sintaxe bem definida; Como o objetivo da WebSemântica é tornar os documentos da Web mais fáceis de serem processados por máquinas,este é um requisito básico. ii) semântica formal; Descrever a base de conhecimento de formalogicamente precisa é fundamental para fazer inferências como dedução de conceitos, checa-gem de consistência na base de conhecimento e instanciação de indivíduos a uma classe. iii)suporte a raciocínio; Uma vez que a linguagem possui uma semântica formal, atividades de

1sitio oficial: http://w3.org


Nome Sintaxe Semântica ExpressividadeVerdade > ∆ι ALAbsurdo ⊥ /0 ALConceito C Cι ⊆ ∆ι ALRelação R Rι ⊆ ∆ιx∆ι ALInterseção CuD Cι ∩Dι ALUnião CtD Cι ∪Dι UNegação ¬C ∆ι\Aι CRestrição de valor ∀R.C {a ∈ ∆ι |∀b.(a,b) ∈ Rι → b ∈Cι} ALRestrição existencial ∃R.C {a ∈ ∆ι |∃b.(a,b) ∈ Rι ∧b ∈Cι} ε

Restrição ≥ nR {a ∈ ∆ι ||{b ∈ ∆ι |(a,b) ∈ Rι}| ≥ n}numérica ≤ nR {a ∈ ∆ι ||{b ∈ ∆ι |(a,b) ∈ Rι}| ≤ n} Nnão qualificada = nR {a ∈ ∆ι ||{b ∈ ∆ι |(a,b) ∈ Rι}|= n}Restrição ≥ nR.C {a ∈ ∆ι ||{b ∈ ∆ι |(a,b) ∈ Rι ∧b ∈Cι}| ≥ n}numérica ≤ nR.C {a ∈ ∆ι ||{b ∈ ∆ι |(a,b) ∈ Rι ∧b ∈Cι}| ≤ n} Qqualificada = nR.C {a ∈ ∆ι ||{b ∈ ∆ι |(a,b) ∈ Rι ∧b ∈Cι}|= n}

Tabela 2.2 Sintaxe e semântica de alguns contructos de lógica de descrição com anotação de expressi-vidade

raciocínio podem ser realizadas. iv) expressividade; alguns domínios precisam de construtosmais elaborados para que possam ser descritos. Quanto maior a expressividade da linguagem,naturalmente fica mais fácil de descrever um domínio, apesar de aumentar a complexidade etempo de processamento.

Entre os requisitos citados no parágrafo anterior estão expressividade e suporte a racio-cínio. Apesar de ambos poderem estar na linguagem, são antagônicos, quanto maior for aexpressividade da linguagem, mais complexas e demoradas serão as atividades de raciocíniosobre a linguagem. Para criar fronteiras nesse conflito entre expressividade e complexidade deraciocínio, a w3c criou três versões de OWL: OWL Full, OWL DL e OWL Lite.

2.2.1 OWL Full

A Web Ontology Language em sua versão mais expressiva, usando todas as primitivas da lin-guagem, é chamada de OWL Full. Essa combinação inclui, por exemplo, aplicar uma restriçãode cardinalidade na classe que contém todas as outras classes, limitando a quantidade de classesque a ontologia pode ter.

OWL Full é completamente compatível com RDF, tanto sintaticamente, quanto em suasemântica. A desvantagem de OWL Full é que ela é tão poderosa que é indecidível em relaçãoàs atividades de raciocínio.


2.2.2 OWL DL

OWL DL (DL é a sigla para Description Logic, Lógica de Descrição em português) é a famíliade OWL que corresponde à lógica de Descrição. A sua grande vantagem é que ela é decidível,dando a possibilidade de realização de atividades de raciocínio de forma mais eficiente. Adesvantagem de OWL DL é que ela perde a compatibilidade com RDF, qualquer documentoem OWL DL pode ser descrito como um documento em RDF, mas o contrário não é verdade.

2.2.3 OWL Lite

OWL Lite é uma família de OWL que é mais limitada do que OWL Full e OWL DL. Ela nãodá suporte a, por exemplo, disjunção entre classes, união e complemento. A grande vanta-gem dessa linguagem é uma maior facilidade para o desenvolvimento de ferramentas, e a suadesvantagem é a perda de expressividade.

CAPÍTULO 3

Normalização para o método das conexões

O método das conexões proposto por W. Bibel [Bib82] é um método para prova automática deteoremas descritos em lógica de primeira ordem [BH93]. Um dos trabalhos recentes de Freitaset al [FSS10] foi a extenção desse método para lógica de descrição ALC.

O artigo intitulado A Connection Method for Reasoning with the Description Logic ALC[FSS10] propõe algoritmos tanto para o método, quanto para a normalização que precisa serfeita na base de conhecimento para que seja possível a representação necessária para o métododas conexões usando apenas uma matriz.

O objetivo deste trabalho é implementar algum algoritmo de normalização para o métododas conexões como os citados no texto de Freitas et al. Dois algoritmos foram propostos comesse objetivo [FSS10]; o primeiro utiliza-se de uma tabela com nove regras que devem seraplicadas à base de conhecimento a fim de obter a forma normal positiva. O segundo, intitulado"A more complex and efficient normalization"não cria novos símbolos durante a sua execução,fazendo-o mais eficiente que o primeiro em relação ao uso de memória.

No cronograma deste trabalho estava prevista a implementação desse segundo algoritmo,porém, ao decorrer do desenvolvimento, propomos um terceiro algoritmo que é ainda maiseficiente em relação ao uso de memória, ele é linear em relação à quantidade de impurezas nabase, enquanto que o "A more complex and efficient normalization"é quadrático. O restantedesse capítulo se dedicará a dar definições para o entendimento dos últimos dois algoritmoscomentados acima e também descrevá as suas implementações.

3.1 Tradução de ontologias ALC para forma normal disjuntiva

Para que o leitor consiga entender melhor os algoritmos de tradução, alguns conceitos precisamser fixados.

Métodos diretos como o método das conexões são formulados para provar que uma fórmulaou um conjunto de fórmulas é um teorema, sse cada interpretação gerada é uma tautologia.Tautologias normalmente tomam a forma L∨¬L, nesse caso, a fórmula precisa estar na FormaNormal Disjuntiva (ou, do inglês, Disjunctive Normal Form - DNF).

Definição 1 (Forma Normal Disjuntiva, cláusula). Uma fórmula em DNF é uma conjunção dedisjunções. Ou seja, tomam a forma:

n⋃i=1

Ci , ou, C1∨ ...∨Cn.

onde cada Ci é uma cláusula. Uma cláusula é uma conjunção de literais. Ou seja, tomam aforma:

10

3.1 TRADUÇÃO DE ONTOLOGIAS ALC PARA FORMA NORMAL DISJUNTIVA 11

m⋂j=1

Li, j , ou, Li,1∧ ...∧Li,m , também representado por {Li,1, ...,Li,m}

onde cada Li, j é um literal, resultando na fórmula:

n⋂i=1

m⋃j=1

Li, j , ou, (L1,1∧ ...∧L1,m)∨ (Ln,1∧ ...∧Ln,m)

podendo ser chamada também de forma causal disjuntiva, representada por:

{{(L1,1, ...,L1,m}, ...,{Ln,1, ...,Ln,m}}

A definição acima é a definição herdada da lógica de primeira ordem, para ser válida tam-bém para a lógica de descrição o conceito de conjunções e disjunções deve ser estendido.

Definição 2 (Conjunção ALC). Uma conjunção ALC é um literal L, uma conjunção (E0∧, ...,∧En),ou uma restrição existencial ∃x.E, onde E é uma expressão qualquer em lógica de descrição.

Definição 3 (Disjunção ALC). Uma disjunção ALC é um literal L, uma disjunção (E0∨, ...,∨En),ou uma restrição de valor ∀x.E, onde E é uma expressão qualquer em lógica de descrição.

Definição 4 (Conjunção ALC pura, Conjunção ALC não pura). Uma conjunção ALC pura éuma conjunção ALC que na forma normal negada não contém restrições de valor (∀x.E) e tam-bém não contém disjunções (E∨, ...,∨E). O conjunto de conjunções ALC puras é representadopor C. Uma conjunção ALC não pura é uma conjunção ALC que não é pura.

Definição 5 (Disjunção ALC pura, Disjunção ALC não pura). Uma disjunção ALC pura é umadisjunção ALC que na forma normal negada não contém restrições existenciais (∃x.E) e tam-bém não contém conjunções (E∧, ...,∧E). O conjunto de disjunções ALC puras é representadopor D. Uma disjunção ALC não pura é uma disjunção ALC que não é pura.

Definição 6 (Impureza em uma expressão não pura). Impureza em expressões ALC não purassão conjunções em disjunções não puras ou disjunções em conjunções não puras. O conjuntode impurezas é chamado de conjunto de impurezas ALC e é representado por I.

Definição 7 (Forma Normal Positiva). Um axioma ALC está na Forma Normal Positiva sse eleestá em uma das seguintes formas:

i) Av Cii) Dv Aiii) C v D

onde A é um conceito atômico, C é uma conjunção ALC pura, D é uma disjunção ALCpura.


O método das conexões utiliza matrizes para realizar provas de teoremas. No início destetrabalho, ainda não era possível fazer as provas com matrizes aninhadas, ou seja, havia semprea necessidade de normalizar a base de conhecimento na forma normal positiva (definição 7).No entanto, Jens Otten em um trabalho entitulado A Non-clausal Connection Calculus [Ott11]mostrou como aplicar o método das conexões sem o passo da normalização. Apesar da recenteevolucão do método, para o objetivo deste trabalho, ainda é necessário fazer a normalização, jáque para lógica de descrição, o método ainda não foi modificado para usar matrizes aninhadas.

A próxima seção desta monografia descreve o algoritmo que propomos para a normalizaçãopara a forma normal positiva.

3.1.1 Algoritmo Proposto

Esta seção da monografia descreve a implementação realizada neste trabalho.O método das conexões é um método direto, ou seja, uma consulta à base de conhecimento

verifica se uma fórmla é uma tautologia e toma a forma KB→ α , onde α é um axioma e KB

(Knowledge base) é da forman⋂

i=1Ai, onde Ai também é um axioma. Expandindo a fórmula

¬KB∨α , temos:

¬n⋂

i=1Ai∨α [ou, ¬(A1∧ ...∧An)∨α], que pode ser transformada para:

n⋃i=1¬Ai∨α [ou, ¬A1∨ ...∨¬An∨α]

Cada Ai ou α precisam estar na forma normal positiva, ou seja, precisam estar em uma dasformas: i) Av C, ii) Dv A, ou, iii) C v D, onde A é um conceito, C é uma conjunção pura e Dé uma disjunção pura.

O primeiro passo do algoritmo é a separação de axiomas de equivalência de expressões einclusões. Os axiomas de equivalência serão substituídos por dois axiomas de inclusão, e.g.,(A≡ B→ Av B∧Bv A).

Algorithm 1 Normalize-Ontology(O)Require: O: ontologia em lógica de descrições ALC

1. for all A v B ∈ SI do {A, B são expressões, SI é o conjunto dos axiomas de inclusãopertencentes a O}

2. Normalize-Axiom (Av B)3. end for4. for all A≡B∈ SEQ do {A, B são expressões, SEQ é o conjunto dos axiomas de equivalência

pertencentes a O}5. Normalize-Axiom (Av B)6. Normalize-Axiom (Bv A)7. end for

Algorithm 2: O método Normalize-Axiom(Av B) remove o axioma da ontologia (linha 1),remove as impurezas do dado esquedo (linha 2) e do lado direto (linha 3) do axioma. Casoele já esteja na forma normal positiva (linha 3) apenas pela remoção das impurezas, ele será


adicionado à base novamente (linha 5), caso contrário, dois axiomas serão criados, um com aexpressão do lado esquerdo (linha 7) e outro com a expressão do lado direito (linha 8). Casoesses novos axiomas sejam criados, eles já estarão na forma normal positiva, já que uma ex-pressão pura em uma relação de inclusão com um conceito está na forma normal positiva emqualquer combinação.

Algorithm 2 Normalize-Axiom (Av B)Require: Av B: inclusão de A em B

1. O = {O− (Av B)}2. pure_le f t = purify (A, le f t)3. pure_right = purify (B,right)4. if (pure_le f t v pure_right) ∈ SPNF then {SPNF é o conjunto das fórmulas na forma nor-

mal positiva}5. O = {O∪ (pure_le f t v pure_right)}6. else7. O = {O∪ (pure_le f t v N)}8. O = {O∪ (N v pure_right)}9. end if

Algorithm 3: O método purify (e, side) recebe uma expressão em DL ALC e a retorna semimpurezas. O parâmetro side é necessário para remoção de uma impureza, caso a impurezaesteja no lado esquerdo, e.g., Cu ImpurityuCuCv A, um axioma será criado com a impurezado lado esquerdo, e.g., (CuNewConcept uCuC v A)∧ (Impurity v NewConcept), caso aimpureza esteja no lado direito, o comportamento será o mesmo mas de forma simétrica, oseja, um axima do tipo NewConcept v Impurity será criado e a impureza será substituída porum novo conceito (NewConcept).

As impurezas são identificadas através dos métodos visit. A primeira chamada para esseconjunto de métodos é na linha 3 do método purity, caso a expressão de entrada seja umaconjunção não pura, ou na linha 5 do método purify caso a expressão seja uma disjunção nãopura. O método visit em sua implementação em Java 1 utiliza o padrão de projetos visitor, quepermite criar novas operações sem mudar a definição das estruturas de dados [GHJV95].

Uma pilha chamada expressions_stack é usada no método pois em uma implementaçãoem Java os métodos que visitam cada nó da ontologia não podem retornar objetos por umalimitação da biblioteca OWLAPI 3.0 2 3.

Algorithm 4: O método Extract-Impurity() é usado para criar um novo axioma na ontologiacom a impureza achada por um dos métodos visit. O parâmetro side é utilizado para saber emqual lado do axioma a impureza deverá ficar. Após o a criação do axioma, o método Normalize-Axiom() é chamado com o novo axioma para garantir que ele também esteja na forma normalpositiva.

1código disponível em: http://github.com/adrianomelo/tg2documentação do método visit: http://owlapi.sourceforge.net/javadoc/org/semanticweb/owlapi/model/ OWL-

ClassExpressionVisitor.html3javadoc da documentação da OWLAPI 3.0: http://owlapi.sourceforge.net/javadoc/


Algorithm 3 purify (e, side)Require: e: uma expressão em DL ALCRequire: side: é le f t ou right

1. expressions_stack = STACK()2. if e ∈ Snpc then {Snpc é o conjunto das conjunções não puras}3. visit (expressions_stack, e, side, con junction)4. else if e ∈ Snpd then {Snpd é o conjunto das disjunções não puras}5. visit (expressions_stack, e, side, dis junction)6. end if7. return POP (expressions_stack)

Algorithm 4 Extract-Impurity (e, side)Require: e: uma expressão em DL ALCRequire: side: é le f t ou right

1. N = NEW-CONCEPT()2. if side = le f t then3. O = {O∪ (ev N)}4. Normalize-Axiom(ev N)5. else6. O = {O∪ (N v e)}7. Normalize-Axiom(N v e)8. end if9. return N


Algorithm 5, 6, 7, 8, 9, 10: O conjunto de métodos chamados de visit diferem em qual

expressão em lógica de descrições cada um suporta. O método visit (stack,n⋃

ei, side, kind), porexemplo, dá suporte às uniões entre expressões.

Quatro parâmetros são passadados para os métodos, uma pilha stack que é usada para auxi-liar a construção de uma nova expressão normalizada (os métodos não podem retornar objetospor uma limitação da OWLAPI 3.0, biblioteca usada na implementação em Java). Uma expres-

são em lógica de descrições, que pode ser uma uniãon⋃

ei, interseçãon⋂

ei, restrição de valor∀rE, restrição existencial ∃rE, complemento ¬e ou conceito C. O lado side em que a expressãooriginal estava (left ou right). E o tipo kind de expressão que o método estava esperando.

Quando uma conjunção é passada para o método visit e o tipo (kind) é igual a disjunc-tion, significa que uma impureza foi encontrada e ela deve ser removida pelo método Extract-Impurity(). De forma análoga, quando uma disjunção é visitada por um dos métodos visit e otipo esperado é conjunction, significa que uma impureza foi encontrada e ela deve ser removidapelo método Extract-Impurity().

Algorithm 5 visit (stack,n⋃

ei, side, kind)Require: stack: uma pilhaRequire: side: é le f t ou right

Require:n⋃

ei: união de expressões ei1. if kind = con junction then2. N = Extract-Impurity(

n⋃ei, side)

3. PUSH (stack, N)4. else5. for all ei ∈

n⋃ei do

6. visit (stack, ei, side, kind)7. end for8. PUSH (stack,

n⋃POP(stack))

9. end if

Para uma melhor comparação da matrizes que são geradas com o algoritmo proposto, oexemplo que Freitas et al [FSS10] também será o exemplo deste agoritmo. O axioma de equi-valencia no Exemplo 1 é a base de conhecimento usada.

Exemplo 1. Deseja-se normalizar o axioma:

PizzaMargherita≡ Pizzau∃hasTopping.Tomateu∃hasTopping.Muzzarellau¬∃hasTopping.¬(TomatetMuzzarella)

O primeiro passo do algoritmo (método Normalize-Ontology(), página 12) separa o axiomade equivalência em dois axiomas de inclusão. Obtendo-se então:

PizzaMargheritav Pizzau∃hasTopping.Tomateu∃hasTopping.Muzzarellau¬∃hasTopping.¬(TomatetMuzzarella)


Algorithm 6 visit (stack,n⋂

ei, side, kind)Require: stack: uma pilhaRequire: side: é le f t ou right

Require:n⋂

ei: interseção de expressões ei1. if kind = dis junction then2. N = Extract-Impurity(

n⋃ei, side)

3. PUSH (stack, N)4. else5. for all ei ∈

n⋂ei do

6. visit (stack, ei, side, kind)7. end for8. PUSH (stack,

n⋂POP(stack))

9. end if

Algorithm 7 visit (stack, ∀rE, side, kind)Require: stack: uma pilhaRequire: side: é le f t ou rightRequire: ∀rE: restrição de valor com a relação r e a expressão E

1. if kind = con junction then2. N = Extract-Impurity(

n⋃ei, side)

3. PUSH (stack, N)4. else5. E ′ = NNF(E)6. visit (stack, E ′, side, kind)7. E ′′ = POP(stack)8. PUSH (stack, ∀rE ′′)9. end if

Algorithm 8 visit (stack, ∃rE, side, kind)Require: stack: uma pilhaRequire: side: é le f t ou rightRequire: ∃rE: restrição existencial com a relação r e a expressão E

1. if kind = dis junction then2. N = Extract-Impurity(

n⋃ei, side)

3. PUSH (stack, N)4. else5. E ′ = NNF(E)6. visit (stack, E ′, side, kind)7. E ′′ = POP(stack)8. PUSH (stack, ∃rE ′′)9. end if


Algorithm 9 visit (stack, ¬e, side, kind)Require: stack: uma pilhaRequire: side: é le f t ou rightRequire: ¬e: negação de uma expressão e

1. if E /∈ Sconcept then2. e′ = NNF(¬e)3. visit (stack, e′, side, kind)4. else5. PUSH(stack, ¬e)6. end if

Algorithm 10 visit (stack, C, side, kind)Require: stack: uma pilhaRequire: side: é le f t ou rightRequire: C: é um conceito

1. PUSH (stack, C)

Pizzau∃hasTopping.Tomateu∃hasTopping.Muzzarellau¬∃hasTopping.¬(TomatetMuzzarella)v PizzaMargherita

O método Normalize-Axiom() será chamado então com cada um dos axiomas obtidos. Olado direito no primeiro axioma e o lado esquerdo do segundo são conjunções, então o métodovisit de interseções será chamado com o kind sendo conjunction tanto para a primeira expressãoquanto para a segunda.

Quando o método visit (stack, ¬e, side, kind) for chamado com a expressão¬∃hasTopping.¬(TomatetMuzzarella), tanto para o lado esquerdo, quanto para o lado direito ele a transformará na ex-pressão ∀hasTopping.(TomateuMuzzarella), que é uma disjunção. Os axiomas que serãoobtidos são:

PizzaMargheritav Pizzau∃hasTopping.Tomateu∃hasTopping.MuzzarellauExtracted1Extracted1v ∀hasTopping.(TomatetMuzzarella)

Pizzau∃hasTopping.Tomateu∃hasTopping.MuzzarellauExtracted2v PizzaMargherita∀hasTopping.(TomatetMuzzarella)v Extracted2

Em formato matricial, temos (axiomas 1 e 2):

PM PM PM PM PM PM Extracted1¬Pizza ¬hasTopping ¬Tomate ¬hasTopping ¬Muzzarella ¬Extracted1 ¬hasTopping

¬Tomate¬Muzzarella

e (axiomas 3 e 4):


Pizza ¬hasTopping Tomate MuzzarellahasTopping ¬Extracted2 ¬Extracted2 ¬Extracted2

TomatehasToppingMuzzarellaExtracted2

¬PizzaMargherita

O algoritmo de Freitas et al [FSS10] chegou às mesmas matrizes. O que indica que ambos

são lineares em relação às impurezas deste exemplo.

Exemplo 2. No exemplo dado por Freitas et al [FSS10], o seu algoritmo se comportava deforma linear (em espaço) em relação às impurezas nas expressões. Porém, com o caso C v D,onde C e D são conjunções puras, o algoritmo se comporta de forma quadrática em relação amemória.

O algoritmo proposto irá dividir o axioma em dois, ficando C v A, e Av D. Já o algoritmode Freitas et al, irá construir vários axiomas, um para cada expressão do lado direito, e.g.,{C v D1,C v D2, ...,C v Dm−1,C v Dm}. O que irá resultar em uma matriz do tipo:

C1 C1 . . . C1 C1C2 C2 . . . C2 C2...

... . . . ......

Cn−1 Cn−1 . . . Cn−1 Cn−1Cn Cn . . . Cn Cn¬D1 ¬D2 . . . ¬Dm−1 ¬Dm

enquanto que o algoritmo proposto irá produzir uma matriz do tipo:

C1 A A . . . A AC2 ¬D1 ¬D2 . . . ¬Dm−1 ¬Dm...

Cn−1Cn¬A

3.1.2 Algoritmo Original

Esta seção contém o algoritmo escrito por Freitas et al [FSS10] para a normalização de basesde conhecimento em lógica de descrição ALC. A figura 3.1 descreve o método Normalize-Ontology (), que chama os métodos Normaize-LHS () e Normalize-RHS () caso o lado esquerdoe direito, respectivamente, não estejam normalizados para cada axioma da ontologia.

Os métodos Normalize-LHS () e Normalize-RHS são duais, ou seja, possuem a mesmalógica mas com o sentido invertido. A figura 3.2 mostra o pseudocódigo do método Normalize-LHS() e a figura 3.3 mostra o pseudocódigo do método Normalize-RHS.


Figura 3.1 Método Normalize-Ontology ()

Figura 3.2 Método Normalize-LHS ()


Figura 3.3 Método Normalize-RHS ()


Note que o primeiro algoritmo da seção 3.1.1 e a figura 3.1 são praticamente o mesmo,porém, o primeiro diferencia dentro do método os axiomas de equivalência e inclusão. Noartigo de Freitas et al [FSS10] é citado que isso deve ser feito, mas não explicita no algoritmo.

CAPÍTULO 4

leanCoP

O leanCoP é um provador automático de teoremas para lógica de primeira ordem escrito emProlog [OB03]. Em testes realizados com a biblioteca TPTP [Sut09], o leanCoP mostrou boaperformance, mesmo comparado a provadores de teoremas que são estado da arte. Dentre os2200 problemas inclusos na biblioteca TPTP, o leanCoP foi capaz de resolver 667 (30.3%), 532problemas a mais que o leanTAP [BP94] e 932 a menos que o Otter [Mcc95].

O objetivo do uso do leanCoP neste trabalho é validar o algoritmo de normalização descritoem 3.1.1, caso o leanCoP consiga ser usado com a base de conhecimento descrita em ALC,significa que os axioms da base estão na forma normal positiva.

É importânte notar que a ontologia OWL, documento que contém os axiomas da base deconhecimento, é descrita em lógica de descrição. Algumas ferramentas se mostraram necessá-rias para que essa base em OWL fosse usada com o leanCoP. Primeiro, a ontologia é convertidapara o formato TPTP a partir da biblioteca owlapi 1.0 1, o arquivo gerado passa então poruma transformação para que use a linguagem de lógica de primeira ordem do TPTP. Após essatransformação, os axiomas da base podem ser utilizadas pelo leanCoP.

Os códigos abaixo mostram exemplos da linguagem usada pelo leanCoP:

fof(axiom_13,axiom,(! [X] :

( iAB(X)<=> ( iA(X)

| iB(X) ) ) )).

O exemplo acima é um axioma expresso em lógica de primeira ordem que é equivalente a:

∀x(AB(x) ⇐⇒ A(x)∨B(x))

A owlapi, biblioteca que transforma de OWL para TPTP, define em lógica de primeiraordem alguns conceitos básicos que são necessários para que os teoremas separem o domíniodas intâncias de classes do domínio dos tipos pre-definidos em OWL. o exemplo de códigoabaixo mostra três dos onze axiomas que são gerados pela biblioteca com esse objetivo:

fof(axiom_0,axiom,(! [X] :

( abstractDomain(X)

1download: http://sourceforge.net/projects/owlapi/files/OWL%20API%20%28OWL%201.0%29/

22

CAPÍTULO 4 LEANCOP 23

| dataDomain(X) ) )).

fof(axiom_1,axiom,(? [X] : abstractDomain(X) )).

fof(axiom_2,axiom,(? [X] : dataDomain(X) )).

O primeiro axioma é igual a ∀x(abstractDomain(x)∨ dataDomain(x)), ou seja, todos oselementos do domínio ou são abstractDomain ou dataDomain. O segundo axioma é igual a∃x(abstractDomain(x)), ou seja, o domínio abstractDomain não é vazio. E o terceiro axiomado exemplo é igual a ∃x(dataDomain(x)), ou seja, o domínio dataDomain também não é vazio.Abaixo estão todos os axiomas que são básicos para todas as bases:

∀x(abstractDomain(x)∨dataDomain(x))

∃x(abstractDomain(x))

∃x(dataDomain(x))

∀x¬(abstractDomain(x)∧dataDomain(x))

∀x(owlT hing(x) =⇒ abstractDomain(x))

∀x(owlNothing(x) =⇒ abstractDomain(x))

∀x(abstractDomain(x) =⇒ owlT hing(x))

∀x¬(owlNothing(x))

∀x(xsd_string(x) =⇒ dataDomain(x))

∀x(xsd_integer(x) =⇒ dataDomain(x))

∀x(dataDomain(x) =⇒ ¬(xsd_string(x)∧ xsd_integer(x))

Para fazer alguma atividade de raciocínio a partir dessa base, um número exponencial deconsultas deveria ser gerado. Subsunsão, por exemplo, consistirá em perguntar se cada conceitopode ser sub-classe de outro conceito.

Devido a essa solução ser muito ineficiente, devido à quantidade transformações de arquivosque cada consulta deveria gerar, essa atividade de consulta acaba fugindo do escopo desseprojeto, que é a implementação do algoritmo de normalização para o Método das Conexõescom ontologias ALC.

CAPÍTULO 5

Conclusão e trabalhos futuros

5.1 Conclusão

Os resultados de boa performance do leanCoP para lógica de primeira ordem dão indícios que ométodo das conexões pode ganhar espaço entre os métodos de prova para lógica de descrição.Como a w3c 1 ainda não definiu uma tecnologia padrão para a camada de lógica e prova daWeb Semântica, trabalhos como o que este está inserido são de importância estratégica para aWeb, eles desenvolvem soluções que poderão ser adotados em larga escala pelo mundo.

O leanCoP foi envolvido neste trabalho para realizar atividades de raciocínio, como sub-sunção e equivalência, após a normalização da base de conhecimento. O leanCoP é escritoem Prolog e as APIs de manipulação de ontologias OWL são escritas em Java. Para fazer oleanCoP usar como base de conhecimento as ontologias OWL normalizadas, foi utilizado oformato TPTP como linguagem intermediária. Porém, para fazer as atividades de raciocíniode forma automática, um número exponencial de arquivos deveriam ser gerados em TPTP paraserem usados com o leanCoP. Além disso, um trabalho de parsing desses arquivos deveria serrealizado para adicionar cada consulta à base de conhecimento de cada arquivo, o que se mos-trou fora do escopo do projeto. O leanCoP foi utilizado então para fazer simples checagem deconsistência na base de conhecimento, que traz como efeito colateral a validação da corretudedo algoritmo de normalização.

Na proposta inicial deste trabalho estava prevista a implementação do algoritmo de norma-lização de Freitas et al [FSS10], porém, apesar do algoritmo não incluir novos símbolos à basede conhecimento, não é fácil de ser entendido. A seção 3.1.1 mostra em pseudo-código a imple-mentação que foi feita neste trabalho. O algoritmo foi produzido devido a uma provocação desimplificar o algoritmo de Freitas et al [FSS10]. O objetivo dos algoritmos é o mesmo, traduziros axiomas de uma ontologia ALC para a forma normal positiva, mas o algoritmo da seção3.1.1 além de ser mais simples de ser implementado, faz a matriz gerada após a normalizaçãoconsumir menos memória, o que foi uma grande contribuição. A redução do uso de memóriavai impactar no tempo de execução do método das conexões para lógica de descrição, já que abusca pelos caminhos na matriz vai ser reduzido.

5.2 Trabalhos futuros

Este trabalho não contempla todos os constructos de OWL, nem sequer de OWL Lite, já queé limitada à familia ALC. Trabalhos futuros serão para estender o algoritmo de normalização

1site: http://w3.org

24

5.2 TRABALHOS FUTUROS 25

para incluir restrições com cardinalidade, domínio e contradomínio de propriedades, disjunçãoentre classes e assim por diante.

Este trabalho é apenas um dos módulos necessários para a implementação de um racioci-nador escrito em java que use o método das conexões. O algoritmo em si que procura pelasconexões, ou caminhos, ainda não foi implementado.

E, por fim, quando o método das conexões estiver formalizado para uma família de DL queseja equivalente a uma família de OWL e a sua implementação estiver finalizada, poderá haverum trabalho para integrar o raciocinador a editores de ontologias existentes no mercado, comoo Protégé.

Referências Bibliográficas

[AH08] Grigoris Antoniou and Frank van Harmelen. A Semantic Web Primer, 2nd Edition(Cooperative Information Systems). The MIT Press, 2 edition, 2008.

[BCM+03] Franz Baader, Diego Calvanese, Deborah McGuinness, Daniele Nardi, and PeterPatel-Schneider, editors. The Description Logic Handbook: Theory, Implementa-tion and Applications. Cambridge University Press, Cambridge, 2003.

[Bez95] Jeff Bezos. amazon.com, 1995.

[BH93] W. Bibel and S. Hölldobler. Deduction: automated logic. Academic Press, 1993.

[Bib82] W. Bibel. Automated theorem proving. F. Vieweg, 1982.

[BL89] Tim Berners-Lee. Information management: A proposal, 1989.

[BM11] Kai Brünnler and George Metcalfe, editors. Automated Reasoning with AnalyticTableaux and Related Methods - 20th International Conference, TABLEAUX 2011,Bern, Switzerland, July 4-8, 2011. Proceedings, volume 6793 of Lecture Notes inComputer Science. Springer, 2011.

[BP94] B. Beckert and J. Posegga. Leantap : Lean tableau-based theorem proving. 1994.

[FSS10] Fred Freitas, Anne Schlicht, and Heiner Stuckenschmidt. A connection method forreasoning with the description logic alc. Technical report, UFPE and University ofMannheim, 2010.

[Gal99] Marcos Galperin. mercadolivre.com.br, 1999.

[GHJV95] Erich Gamma, Richard Helm, Ralph Johnson, and John Vlissides. Design pat-terns: elements of reusable object-oriented software. Addison-Wesley Professio-nal, 1995.

[Hef04] Jeff Heflin. Owl web ontology language use cases and requirements. 2004.

[Mcc95] W. Mccune. The otter theorem prover. 1995.

[OB03] Jens Otten and Wolfgang Bibel. leancop: lean connection-based theorem proving.J. Symb. Comput., 36(1-2):139–161, 2003.

26

REFERÊNCIAS BIBLIOGRÁFICAS 27

[Ott11] Jens Otten. A non-clausal connection calculus. In Brünnler and Metcalfe [BM11],pages 226–241.

[RBML99] Romero Rodrigues, Rodrigo Borges, Ronaldo Morita, and Mario Letelier. bus-cape.com.br, 06 1999.

[RN02] Stuart Russell and Peter Norvig. Artificial Intelligence: A Modern Approach (2ndEdition). Prentice Hall series in artificial intelligence. Prentice Hall, 2 edition,December 2002.

[Sic] Carlos Alberto Sicupira. americanas.com.

[Sut09] G. Sutcliffe. The TPTP Problem Library and Associated Infrastructure: The FOFand CNF Parts, v3.5.0. Journal of Automated Reasoning, 43(4):337–362, 2009.

Technology

Trabalho de Graduação: Normalização de ontologias em lógica de descrições para o raciocínio com o provador de teoremas leanCoP