Cette thèse étudie la théorie de la correspondance et la théorie des preuves pour la logique modale monotone et les logiques qui en sont proches.La première partie de la thèse établit une connexion formelle entre la théorie de la correspondance algorithmique et des résultats de caractérisation duale pour les treillis finis, similaire à la caractérisation par Nation d'une hiérarchie de variétés de treillis qui généralise les treillis distributifs. Cette connexion formelle est établie en utilisant la logique modale monotone. Nous adaptons l'algorithme ALBA pour la correspondance à l'environnement de la logique modale monotone, et nous utilisons un encodage, induit par une dualité, des treillis finis sous forme de 'neighbourhood frames' pour traduire les termes de la théorie des treillis en formules de la logic modal monotone.La deuxième partie de la thèse étend la théorie des 'display calculi' à la logique Baltag-Moss-Solecki pour les actions épistémiques et la connaissance (Epistemic Actions and Knowledge), à la logique modale monotone et à la logique propositionnelle dynamique (PDL). Nos résultats incluent plusieurs méta-théorèmes d'élimination de la coupure qui généralisent le théorème original de Belnap dans des dimensions différentes et indépendantes. Les deux principales généralisations des 'display calculi' traitées dans la thèse sont : la généralisation d'une théorie pour les langages ne contenant qu'un seul type à une théorie pour les langages contenant plusieurs types, et la généralisation d'une théorie pour les calculs satisfaisant la propriété de 'display' aux calculs ne la satisfaisant pas. / The present thesis focuses on Monotone Modal Logic and closely related logics from the point of view of Correspondence Theory and Proof Theory.The first part of the thesis establishes a formal connection between algorithmic corre- spondence theory and certain dual characterization results for finite lattices, similar to Nation's characterization of a hierarchy of pseudovarieties of finite lattices progressively generalizing finite distributive lattices. This formal connection is established through monotone modal logic. Specifically, we adapt the correspondence algorithm ALBA to the setting of monotone modal logic, and we use a certain duality-induced encoding of finite lattices as monotone neighbourhood frames to translate lattice terms into formulas in monotone modal logic.The second part of the thesis extends the theory of display calculi to Baltag-Moss- Solecki's logic of Epistemic Actions and Knowledge (EAK), Monotone Modal Logic (MML), and Propositional Dynamic Logic (PDL). Our results include several cut-elimination metatheorems, which generalize the original metatheorem of Belnap in different and mutually independent dimensions. The two main generalizations of display calculi treated in the thesis are: the generalization from single type to multi-type languages, and from the full or relativized display property to no display property.

Automated deduction procedures for modal logics, and related decidable fragments of first-order logic, are used in many real-world applications. A popular way of obtaining decision procedures for these logics is to base them on semantic tableau calculi. We focus on calculi that use unification, instead of the more widely employed approach of generating ground instantiations over the course of a derivation. The most common type of tableaux with unification are so-called free-variable tableaux, where variables are treated as global to the entire tableau. A long-standing open problem for procedures based on free-variable tableaux is how to ensure fairness, in the sense that "equivalent" applications of the closure rule are prevented from being done over and over again. Some solutions such as using depth-first iterative deepening are known, but those are unnecessary in theory, and not very efficient in practice. This is a main reason why there are hardly any decision procedures for modal logics based on free-variable tableaux. In this thesis, we review existing work on incorporating unification into first-order and modal tableau procedures, show how the closure fairness problem arises, and discuss existing solutions to it. For the first-order case, we outline a calculus which addresses the closure fairness problem. As opposed to free-variable tableaux, closure fairness is much easier to achieve in disconnection tableaux and similar clausal calculi. We therefore focus on using clausal first-order tableau calculi for decidable classes, in particular the two-variable fragment. Using the so-called unrestricted blocking mechanism for enforcing termination, we present the first ground tableau decision procedure for this fragment. Even for such a ground calculus, guaranteeing that depth-first terminations terminate is highly non-trivial. We parametrise our procedure by a so-called lookahead amount, and prove that this parameter is crucial for determining whether depth-first derivations terminate or not. Extending these ideas to tableaux with unification, we specify a preliminary disconnection tableau procedure which uses a non-grounding version of the unrestricted blocking rule.

Nesta tese apresentamos o projeto e a implementação do KEMS, um provador de teoremas multi-estratégia baseado no método de tablôs KE. Um provador de teoremas multi-estratégia é um provador de teoremas onde podemos variar as estratégias utilizadas sem modificar o núcleo da implementação. Além de multi-estratégia, o KEMS é capaz de provar teoremas em três sistemas lógicos: lógica clássica proposicional, mbC e mCi. Listamos abaixo algumas das contribuições deste trabalho: * um sistema KE para mbC que é analítico, correto e completo; * um sistema KE para mCi que é correto e completo; * um provador de teoremas multi-estratégia com as seguintes características: - aceita problemas em três sistemas lógicos: lógica clássica proposicional, mbC e mCi; - tem seis estratégias implementadas para lógica clássica proposicional, duas para mbC e duas para mCi; - tem treze ordenadores que são usados em conjunto com as estratégias; - implementa regras simplificadoras para lógica clássica proposicional; - possui uma interface gráfica que permite a visualização de provas; - é de código aberto e está disponível na Internet em http://kems.iv.fapesp.br; * benchmarks obtidos através da comparação das estratégias para lógica clássica proposicional resolvendo várias famílias de problemas; - sete famílias de problemas para avaliar provadores de teoremas paraconsistentes; * os primeiros benchmarks para as famílias de problemas para avaliar provadores de teoremas paraconsistentes. / In this thesis we present the design and implementation of KEMS, a multi-strategy theorem prover based on the KE tableau inference system. A multi-strategy theorem prover is a theorem prover where we can vary the strategy without modifying the core of the implementation. Besides being multi-strategy, KEMS is capable of proving theorems in three logical systems: classical propositional logic, mbC and mCi. We list below some of the contributions of this work: * an analytic, correct and complete KE system for mbC; * a correct and complete KE system for mCi; * a multi-strategy prover with the following characteristics: - accepts problems in three logical systems: classical propositional logic, mbC and mCi; - has 6 implemented strategies for classical propositional logic, 2 for mbC and 2 for mCi; - has 13 sorters to be used alongside with the strategies; - implements simplification rules of classical propositional logic; - provides a proof viewer with a graphical user interface; - it is open source and available on the internet at http://kems.iv.fapesp.br; * benchmark results obtained by KEMS comparing its classical propositional logic strategies with several problem families; * seven problem families designed to evaluate provers for logics of formal inconsistency; * the first benchmark results for the problem families designed to evaluate provers for logics of formal inconsistency.

The purpose of this study is to investigate how teachers with different educational and subject backgrounds co-exist within the same framework of the same education. Previous research suggests that this teacher composition should lead to conflict. But it does not provide any explanations as to how these conflicts are expressed or managed. To illustrate how potential conflicts are expressed or managed, 12 teachers from various Swedish police educations have been interviewed. The theoretical basis is a merging between institutional logics and inhabitant institutions, as a way to direct analytical focus to what happens on the micro level, between the teachers in their daily work. This analytical level has often been neglected in previous research, and this study is a way to contribute to the research about academic drift. The results show that police education is populated by teachers whom we can understand as carriers of different logics. Two logics emerged as particularly contrasting, which I chose to name police logic and academy logic. This means that the teachers was carriers of different ideologically colored norm structures. The results also indicated that the police students were carriers of the police logic. Despite this, I saw no clear traces of conflict. One explanation for this was that teachers' interaction patterns were limited by the organization of the education. One consequence of this was that the teachers with different educations and subject matter rarely met, and conflicts were avoided. In the concrete teaching situation, the two logics met and the teachers needed to find some form of co-existence, especially in relation to the police students. Using Erving Goffman´s concept of cooling out, I found three different cooling out strategies that the teachers used. A central result was that the logics were superior to the teachers. The important thing for the students was not who taught, but what was taught, and that the teaching contents, in the students’ view, had clear professional relevance.

Description Logics (DLs) are increasingly successful knowledge representation formalisms, useful for any application requiring implicit derivation of knowledge from explicitly known facts. A prominent example domain benefiting from these formalisms since the 1990s is the biomedical field. This area contributes an intangible amount of facts and relations between low- and high-level concepts such as the constitution of cells or interactions between studied illnesses, their symptoms and remedies. DLs are well-suited for handling large formal knowledge repositories and computing inferable coherences throughout such data, relying on their well-founded first-order semantics. In particular, DLs of reduced expressivity have proven a tremendous worth for handling large ontologies due to their computational tractability. In spite of these assets and prevailing influence, classical DLs are not well-suited to adequately model some of the most intuitive forms of reasoning. The capability for abductive reasoning is imperative for any field subjected to incomplete knowledge and the motivation to complete it with typical expectations. When such default expectations receive contradicting evidence, an abductive formalism is able to retract previously drawn, conflicting conclusions. Common examples often include human reasoning or a default characterisation of properties in biology, such as the normal arrangement of organs in the human body. Treatment of such defeasible knowledge must be aware of exceptional cases - such as a human suffering from the congenital condition situs inversus - and therefore accommodate for the ability to retract defeasible conclusions in a non-monotonic fashion. Specifically tailored non-monotonic semantics have been continuously investigated for DLs in the past 30 years. A particularly promising approach, is rooted in the research by Kraus, Lehmann and Magidor for preferential (propositional) logics and Rational Closure (RC). The biggest advantages of RC are its well-behaviour in terms of formal inference postulates and the efficient computation of defeasible entailments, by relying on a tractable reduction to classical reasoning in the underlying formalism. A major contribution of this work is a reorganisation of the core of this reasoning method, into an abstract framework formalisation. This framework is then easily instantiated to provide the reduction method for RC in DLs as well as more advanced closure operators, such as Relevant or Lexicographic Closure. In spite of their practical aptitude, we discovered that all reduction approaches fail to provide any defeasible conclusions for elements that only occur in the relational neighbourhood of the inspected elements. More explicitly, a distinguishing advantage of DLs over propositional logic is the capability to model binary relations and describe aspects of a related concept in terms of existential and universal quantification. Previous approaches to RC (and more advanced closures) are not able to derive typical behaviour for the concepts that occur within such quantification. The main contribution of this work is to introduce stronger semantics for the lightweight DL EL_bot with the capability to infer the expected entailments, while maintaining a close relation to the reduction method. We achieve this by introducing a new kind of first-order interpretation that allocates defeasible information on its elements directly. This allows to compare the level of typicality of such interpretations in terms of defeasible information satisfied at elements in the relational neighbourhood. A typicality preference relation then provides the means to single out those sets of models with maximal typicality. Based on this notion, we introduce two types of nested rational semantics, a sceptical and a selective variant, each capable of deriving the missing entailments under RC for arbitrarily nested quantified concepts. As a proof of versatility for our new semantics, we also show that the stronger Relevant Closure, can be imbued with typical information in the successors of binary relations. An extensive investigation into the computational complexity of our new semantics shows that the sceptical nested variant comes at considerable additional effort, while the selective semantics reside in the complexity of classical reasoning in the underlying DL, which remains tractable in our case.

Cette thèse présente une formalisation en Coq des langages et des algorithmes fondamentaux portant sur les bases de données. Ainsi, ce fourni des spécifications formelles issues des deux approches différentes pour la définition des modèles de données: une basée sur l’algèbre et l'autre basée sur la logique.A ce titre, une première contribution de cette thèse est le développement d'une bibliothèque Coq pour le modèle relationnel. Cette bibliothèque contient les modélisations de l’algèbre relationnelle et des requêtes conjonctives. Il contient aussi une mécanisation des contraintes d'intégrité et de leurs procédures d'inférence. Nous modélisons deux types de contraintes: les dépendances, qui sont parmi les plus courantes: les dépendances fonctionnelles et les dépendances multivaluées, ainsi que leurs axiomatisations correspondantes. Nous prouvons formellement la correction de leurs algorithmes d'inférence et, pour le cas de dépendances fonctionnelles, aussi la complétude.Ces types de dépendances sont des instances de contraintes plus générales : les dépendances génératrices d'égalité (equality generating dependencies, EGD) et, respectivement, les dépendances génératrices de tuples (tuple generating dependencies, TGD), qui appartiennent a une classe encore plus large des dépendances générales (general dependencies). Nous modélisons ces dernières et leur procédure d'inférence, i.e, "the chase", pour lequel nous établissons la correction. Enfin, on prouve formellement les théorèmes principaux des bases de données, c'est-à-dire, les équivalences algébriques, la théorème de l' homomorphisme et la minimisation des requêtes conjonctives.Une deuxième contribution consiste dans le développement d'une bibliothèque Coq/ssreflect pour la programmation logique, restreinte au cas du Datalog. Dans le cadre de ce travail, nous donnons la première mécanisations d'un moteur Datalog standard et de son extension avec la négation. La bibliothèque comprend une formalisation de leur sémantique en theorie des modelés ainsi que de leur sémantique par point fixe, implémentée par une procédure d'évaluation stratifiée. La bibliothèque est complétée par les preuves de correction, de terminaison et de complétude correspondantes. Cette plateforme ouvre la voie a la certification d' applications centrées données. / This thesis presents a formalization of fundamental database theories and algorithms. This furthers the maturing state of the art in formal specification development in the database field, with contributions stemming from two foundational approches to database models: relational and logic based.As such, a first contribution is a Coq library for the relational model. This contains a mechanization of integrity constraints and of their inference procedures. We model two of the most common dependencies, namely functional and multivalued, together with their corresponding axiomatizations. We prove soundness of their inference algorithms and, for the case of functional ones, also completeness. These types of dependencies are instances of equality and, respectively, tuple generating dependencies, which fall under the yet wider class of general dependencies. We model these and their inference procedure,i.e, the chase, for which we establish soundness.A second contribution consists of a Coq/Ssreflect library for logic programming in the Datalog setting. As part of this work, we give (one of the) first mechanizations of the standard Datalog language and of its extension with negation. The library includes a formalization of their model theoretical semantics and of their fixpoint semantics, implemented through bottom-up and, respectively, through stratified evaluation procedures. This is complete with the corresponding soundness, termination and completeness proofs. In this context, we also construct a preliminary framework for dealing with stratified programs. This work paves the way towards the certification of data-centric applications.

I en analys av 300 annonser på en öppen webbplats där socialtjänsten söker efter familjehem till specifika barn kommunicerades fyra olika teman avseende familjehemsuppdraget. Det första temat som avsåg familjens egenskaper förekom i 80 procent av annonserna och det andra temat som gällde förväntningar på uppdragets utförande och familjehemmets kompetens beskrevs i 98 procent av annonserna. Det tredje temat berörde beskrivningar av barnet, hens erfarenheter och egenskaper och förekom i drygt 82 procent av annonserna. När det gällde det fjärde temat- vad familjehemmet kunde förvänta sig i form av utbildning, stöd och ersättning beskrevs det i drygt 35 procent av annonserna. Innehållet i annonserna kan förstås utifrån institutionella logiker om familj, utförande, marknad och solidaritet. Samtidigt förekommande logiker kan erbjuda möjligheter såväl som konflikter och spänningar. Att marknadsföra barn på annons kan bidra till att socialtjänsten kan tillgodose behovet av familjehem, vilket de är ålagda att göra (SOSFS 2012:11). Potentiella familjehem får i tidigt skede information om såväl barnet som förväntningarna på uppdraget och hur socialtjänsten förhåller sig till eventuellt stöd och ersättning. Förfarandet med annonser och dess innehåll kan därmed betraktas som rationellt och effektivt när det gäller utförande av familjehemsuppdraget. Studiens viktigaste bidrag är att konflikter skulle kunna uppstå i mötet mellan en å ena sidan hög förväntan på utförande, kunskap och erfarenhet och å andra sidan en hög förväntan om att ta emot barn av solidariska skäl. Att fokus på stöd och ersättning till familjehemmet är låg, skulle kunna bidra till svårigheter att rekrytera och behålla familjehem. Spänningar skulle också kunna uppstå i mötet mellan socialtjänstens historia av en byråkratisk logik där myndigheten vanligtvis inte delat information om klienter med allmänheten och en marknadslogik där specifika barns egenskaper marknadsförs (anonymt) på öppna webbplatser. Även mötet mellan att se familjehem som en vanlig familj och att ha högt fokus på utförande skulle kunna innebära en konflikt som kan påverka möjligheten att rekrytera familjehem. / In an analysis of 300 advertisements on an open website where the social services are looking for foster homes for specific children, four different themes were communicated regarding the foster home assignment. The first theme, which concerned the family's characteristics, appeared in 80 percent of the advertisements, and the second theme, which concerned expectations of the execution of the assignment and the foster homes competence, was described in 98 percent of the advertisements. The third theme concerned descriptions of the child, her experiences and characteristics and appeared in just over 82 percent of the advertisements. Regarding the fourth theme - what the foster home could expect in the form of education, support and compensation, it was described in just over 35 percent of the advertisements. The content of the ads can be understood from a perspective of institutional logics about family, execution, the market and solidarity. Simultaneously occurring logics can offer opportunities as well as conflicts and tensions. Marketing children through ads can contribute to the social services being able to meet the need for foster homes, which they are obliged to do from the Swedish government (SOSFS: 2012: 11). Potential foster homes receive information at an early stage about both the child and the expectations of the assignment, and how the social services relate to give support and compensation for the foster families. The procedure with advertisements on open websites can thus be considered rational and efficient in the execution of the foster home assignment. The most important contribution of the study is that conflicts could arise in the meeting between a high expectation of execution, knowledge and experience on the one hand and a high expectation of taking care of children in need for solidarity reasons on the other. The low focus on support and compensation for the foster family could contribute to difficulties in recruiting and maintaining foster homes. Tensions could also arise in the meeting between the social services' history of a bureaucratic logic where the authority usually does not make information about clients accessible for the public, and a market logic where specific children's characteristics are marketed (anonymously) on open websites. The meeting between seeing foster homes as an ordinary family and having a high focus on execution could also involve a conflict that might affect the possibility of recruiting foster homes.

Un nombre croissant d'ontologies de grandes tailles ont été développées et mises à disposition dans des référentiels tels que le NCBO Bioportal. L'accès aux connaissances les plus pertinentes contenues dans les grandes ontologies a été identifié comme un défi important. À cette fin, nous proposons dans cette thèse trois notions différentes : modules d’ontologie minimale (sous-ontologies conservant toutes les implications sur un vocabulaire donné), meilleurs extraits ontologiques (certains petits nombres d’axiomes qui capturent le mieux les connaissances sur le vocabulaire permettant un degré de perte sémantique) et un module de projection (sous-ontologies d'une ontologie cible qui impliquent la subsomption, les requêtes d'instance et les requêtes conjonctives issues d'une ontologie de référence). Pour calculer le module minimal et le meilleur extrait, nous introduisons la notion de justification de subsomption en tant qu'extension de la justification (ensemble minimal d'axiomes nécessaires pour conserver une conséquence logique) pour capturer la connaissance de subsomption entre un terme et tous les autres termes du vocabulaire. De même, nous introduisons la notion de justifications de projection qui impliquent une conséquence pour trois requêtes différentes afin de calculer le module de projection. Enfin, nous évaluons nos approches en appliquant une implémentation prototype sur de grandes ontologies. / An increasing number of ontologies of large sizes have been developed and made available in repositories such as the NCBO Bioportal. Ensuring access to the most relevant knowledge contained in large ontologies has been identified as an important challenge. To this end, in this thesis, we propose three different notions: minimal ontology modules (sub-ontologies that preserve all entailments over a given vocabulary), best ontology excerpts (certain, small number of axioms that best capture the knowledge regarding the vocabulary by allowing for a degree of semantic loss) and projection module (sub-ontologies of a target ontology that entail subsumption, instance and conjunctive queries that follow from a reference ontology). For computing minimal module and best excerpt, we introduce the notion of subsumption justification as an extension of justification (a minimal set of axioms needed to preserve a logical consequence) to capture the subsumption knowledge between a term and all other terms in the vocabulary. Similarly, we introduce the notion of projection justifications that entail consequence for three different queries in order to computing projection module. Finally, we evaluate our approaches by applying a prototype implementation on large ontologies.

Le but de cette recherche ethnographique, menée au Pérou à partir de 2008, est de restituer les pratiques, les discours moraux et les multiples stratégies qui sous-tendent l’appropriation des vestiges et des pièces archéologiques par plusieurs acteurs. Cette question est abordée à travers le prisme particulier du trafic d’art et des pratiques considérées comme illicites. Une ethnographie itinérante (Marcus, 1995) et une méthodologie basée sur la biographie des objets (Kopytoff, 1986) permettent dereconstruire le circuit de céramiques, de la production (la fouille clandestine) à laconsommation (l’achat) en passant par leur échange, don et contrefaçon. De trésors à biens culturels, d’artefacts à curiosités, le parcours de ces objets met au jour à la fois la multiplicité de leurs usages socio-politiques et l’évolution des instances delégitimation qui les concernent.La thèse s’intéresse plus particulièrement au département de Lambayeque, situé sur la côte nord, connu pour les remarquables découvertes archéologiques (civilisation Mochica) qui y ont eu lieu au cours des dernières décennies. Elle démontre que, loin d’être les fruits d’un consensus, la patrimonialisation et la mise en tourisme, en tantque ressources économiques et symboliques, peuvent exacerber les conflits, en créantdes dynamiques d’inclusion et exclusion. De fait, l’opposition historique entre conservateurs et destructeurs du patrimoine renforce encore davantage l’asymétrie entre professionnels et communautés porteuses, en termes de savoir et de pouvoir. De plus, le manque de filiation des habitants avec les ancêtres (et donc l’absence de continuité et d’ « authenticité »), jugé par les institutions comme en lien avec une attitude destructive et purement marchande, a entravé une réelle participation de la communauté dans la patrimonialisation. Pour en être reconnus en tant qu’acteurs légitimes, et non comme simples bénéficiaires, ils sont ainsi contraints de reformuler leurs régimes de valeur et de renégocier leurs logiques d’appartenance. / The aim of this ethnographic research, carried out in Peru as of 2008, is to map the practices, moral discourses and multiple strategies which underlie the appropriation of relics and archaeological objects by different actors. This topic is analysed through the prism of art trafficking and practices considered to be illicit. A multi-sited ethnography (Marcus 1995) and a methodology based in the biography of objects (Kopytoff, 1986) allows to reconstruct the circuit of ceramics, from production (clandestine digging) to consumption (purchase), through various forms of exchange, gift and counterfeit. From treasures to cultural goods, from artefacts to oddities, the itinerary of these objects sheds light on the multiplicity of their socio-political uses and the evolution of legitimation authorities concerned by them. The thesis focuses more specifically on the region of Lambayeque, on the northern Peruvian coast, which has been characterised by extraordinary archaeological discoveries (Mochica civilisation) over the last few decades. It shows that, far from being the product of consensus, the heritage making and touristic development, as an economic and symbolical resource, can exacerbate conflicts, creating dynamics of inclusion and exclusion. In fact, the historical opposition between heritage conservationists and destroyers reinforces the asymmetry between professionals and bearer communities, in terms of knowledge and power. Moreover, a destructive attitude and commercial interest in relics, considered as the sign of a lack of filiation and therefore of continuity and « authenticity », hinders inhabitants’ participation. In order to be recognized as legitimate actors, and not as simple beneficiaries of heritage making they are obliged to reformulate their value regimes and renegotiate their logics of belonging.

Dans le contexte du Web sémantique, les ontologies OWL représentent des connaissances explicites sur un domaine sur la base d'une conceptualisation des domaines d'intérêt, tandis que la connaissance correspondante sur les individus est donnée par les données RDF qui s'y réfèrent. Dans cette thèse, sur la base d'idées dérivées de l'ILP, nous visons à découvrir des motifs de connaissance cachés sous la forme de règles d'association multi-relationnelles en exploitant l'évidence provenant des assertions contenues dans les bases de connaissances ontologiques. Plus précisément, les règles découvertes sont codées en SWRL pour être facilement intégrées dans l'ontologie, enrichissant ainsi son pouvoir expressif et augmentant les connaissances sur les individus (assertions) qui en peuvent être dérivées. Deux algorithmes appliqués aux bases de connaissances ontologiques peuplées sont proposés pour trouver des règles à forte puissance inductive : (i) un algorithme de génération et test par niveaux et (ii) un algorithme évolutif. Nous avons effectué des expériences sur des ontologies accessibles au public, validant les performances de notre approche et les comparant avec les principaux systèmes de l'état de l'art. En outre, nous effectuons une comparaison des métriques asymétriques les plus répandues, proposées à l'origine pour la notation de règles d'association, comme éléments constitutifs d'une fonction de fitness pour l'algorithme évolutif afin de sélectionner les métriques qui conviennent à la sémantique des données. Afin d'améliorer les performances du système, nous avons proposé de construire un algorithme pour calculer les métriques au lieu d'interroger viaSPARQL-DL. / In the Semantic Web context, OWL ontologies represent explicit domain knowledge based on the conceptualization of domains of interest while the corresponding assertional knowledge is given by RDF data referring to them. In this thesis, based on ideas derived from ILP, we aim at discovering hidden knowledge patterns in the form of multi-relational association rules by exploiting the evidence coming from the assertional data of ontological knowledge bases. Specifically, discovered rules are coded in SWRL to be easily integrated within the ontology, thus enriching its expressive power and augmenting the assertional knowledge that can be derived. Two algorithms applied to populated ontological knowledge bases are proposed for finding rules with a high inductive power: (i) level-wise generated-and-test algorithm and (ii) evolutionary algorithm. We performed experiments on publicly available ontologies, validating the performances of our approach and comparing them with the main state-of-the-art systems. In addition, we carry out a comparison of popular asymmetric metrics, originally proposed for scoring association rules, as building blocks for a fitness function for evolutionary algorithm to select metrics that are suitable with data semantics. In order to improve the system performance, we proposed to build an algorithm to compute metrics instead of querying via SPARQL-DL.