FREE ELECTRONIC LIBRARY - Dissertations, online materials

«1 Motivation The Ontology Engineering community widely agrees on the importance of helping the user understand the output of a DL reasoner. The most ...»

Beyond Asserted Axioms: Fine-Grain

Justifications for OWL-DL Entailments

Aditya Kalyanpur1 and Bijan Parsia1 and Bernardo Cuenca Grau2

University of Maryland, USA1, University of Manchester, UK2

aditya@cs.umd.edu, bparsia@isr.umd.edu, bcg@cs.man.ac.uk

1 Motivation

The Ontology Engineering community widely agrees on the importance of helping

the user understand the output of a DL reasoner. The most recent approaches to the

problem [4] [3] are based on the notion of a Minimal Unsatisfiability Preserving SubTBoxes (MUPS). Roughly, a MUPS for an atomic concept A is a minimal fragment T ⊆ T of a TBox T in which A is unsatisfiable.

For example, given the TBox:

B ∃R.D E ¬B, 2: C ≥ 1.R 1: A C F ∀R.¬D, 4: B ¬D E 3: A E where the concept A is unsatisfiable, the TBox T = {1} is a MUPS for A in T.

In our earlier work [2], we extended the notion of a MUPS to arbitrary entailments in SHOIN and devised a non-standard inference service, axiom pinpointing, which, given T any of its logical consequences α, determines the minimal fragments of T in which α holds.

However, these services, though useful for debugging and explanation purposes, suffer from a fundamental granularity problem: since they work at the asserted axiom level, they fail to determine which parts of the asserted axioms are irrelevant for the particular entailment under consideration to hold. For instance, in our example, the conjunct E in axiom 1 is irrelevant for the unsatisfiability of A. Moreover, additional parts of axioms that could contribute to the entailment are masked, e.g., the axioms ∃R.D and A ∀R.¬D which also entail the 1, 3 can be broken down into A unsatisfiability of A, however, this condition cannot be captured.

In this paper, we aim at extending the axiom pinpointing service to capture precise justifications, which are at a finer granularity level than the original asserted axioms.

In this context, we provide a formal notion of precise justification and propose a decision procedure for the problem. We discuss implementation details of the service and show that it is feasible in practice. Our results are applicable to SHOIN and hence to OWL-DL.

2 Precise Justifications Since we aim at identifying relevant parts of axioms, we define a function that splits the axioms in a TBox T into “smaller” axioms to obtain an equivalent TBox Ts that contains as many axioms as possible.

Definition 1 (split KB) Given a SHOIN concept C in negation normal form (NNF),

the function split(C) returns a set of concepts, inductively defined as follows:

split(C) ← C, if C is A, ¬A, ≥ n.R, ≤ n.R, = n.R,, ⊥ or a nominal node {o} split(C D) ← split(C) ∪ split(D) split(C D) ← (split(C) ⊗ split(D)) split(∀R.C) ← ∀R. (split(C)) split(∃R.C ) – we get two cases depending on C if C is of the form C D, split(∃R.C ) ← ∃R.E ∪ split(¬E C) ∪ split(¬E D) ∪ split((¬C ¬D) E), where E is a fresh concept else, split(∃R.C ) ← ∃R. split(C ) Given a KB = {α1, α2,...αn }, where each axiom αi is of the form Ci Di, let Cα be the concept representing α, i.e., ¬Ci Di, converted to NNF. Then, Ts = Cs for each concept Cs ∈ split(¬C1 D1 ) ∪ split(¬C2 split KB() = D2 )..split(¬Cn Dn ).

–  –  –

A justification is a generalization of the notion of a MUPS for arbitrary entailments:

Definition 2 (Justification) Let T |= α where α is an axiom. A fragment T ⊆ T is a justification for α in T if T |= α, and T |= α for every T ⊂ T.

We denote by JUST(α, T ) the set of all justifications for α in T.

Finer-grained justifications can be defined as follows:

Definition 3 (Precise Justification) Let T |= α. A TBox T is a precise justification for α in T if T ∈ JUST(α, split TBox(T )).

We denote by JUSTp (α, T ) the set of all precise justifications for α in T.

In SHOIN, entailment can be reduced to concept unsatisfiability. As a consequence, it is easy to show that the problem of finding all the justifications for an unsatisfiable concept and the problem of finding all the justifications for a given entailment can be reduced to each other. In what follows, we shall restrict our attention, without loss of generality, to the problem of finding all the precise justifications for an unsatisfiable concept w.r.t to a SHOIN TBox.

3 Finding Precise Justifications The problem of finding all precise justifications for an entailment α of a TBox T now reduces to the problem of finding all justifications for α in the split T Box(T ). Thus, we can use the algorithm listed in Table 1 to split a TBox, and then apply any decision procedure to find all justifications for the entailment in the split version of the TBox.

We briefly sketch the algorithm we have developed in our earlier work to find all justifications for an arbitrary entailment in a TBox. For details, we refer the reader to the technical report [2].

The first part of the algorithm is based on the decision procedure for concept satisability in SHOIN [1], and it finds any one arbitrary justification for the entailment.

It keeps track of the axioms from the TBox responsible for each change in the completion graph, namely, the addition of a particular concept (or role) to the label of a specific node (or edge), the addition of an equality (merge) or inequality relation between nodes, or the detection of a contradiction (clash) in the label of a node.

In order to ensure correctness, our algorithm imposes an ordering among the deterministic rules: the unfolding and CE rules are only applied when no other deterministic rule is applicable. The rationale for this strategy relies on the definition of justification that establishes minimality w.r.t. the number of axioms considered; the new rules cause new axioms to be considered in the tracing process and additional axioms should only be considered if strictly necessary.

The algorithm works on a tree T of completion graphs. that is incrementally built using the set of available expansion rules, and the traces for the events triggered by the rules are updated on the fly. For a full specification of the expansion rules, we refer the reader to [2]. The application of non-deterministic rules results in the addition of new completion graphs as leaves of T, one for each different non-deterministic choice. However, since C is unsatisfiable w.r.t. T, the algorithm detects a clash in each of the leaves. Upon termination, the trace of the detected clash (or clashes) in the leaves of T yields a justification.

Once a single justification has been found, we find the remaining justifications by employing a variation of the classical Hitting Set Tree (HST) algorithm.

Given a collection S of conflict sets, Reiter’s algorithm constructs a labeled tree

called Hitting Set Tree (HST). Nodes in an HST are labeled with a set s ∈ S and:

1) if H(v) is the set of edge labels on the path from the root to the node v, then L(v) ∩ H(v) = ∅; 2) for each σ ∈ L(v), v has a successor w and L( v, w ) = σ; 3) if L(v) = ∅, then H(v) is a hitting set for S.

In our approach, we form an HST where nodes correspond to single justification sets (computed on the fly), edges correspond to the removal of axioms from the KB, and in building the tree to compute all the minimal hitting sets, we in turn obtain all the justification sets as well. The correctness and completeness of this approach is provided in [2].

–  –  –

4 Implementation Issues We have shown in [3], [2] that the axiom pinpointing service used to find all justications for an entailment of a SHOIN KB performs reasonably well on a lot of real-world OWL-DL ontologies.

The main additional overhead incurred for capturing precise justifications is due to the pre-processing phase where we split the KB. The concern here, from a reasoning point of view, is the introduction of GCIs during the splitting process, e.g. A ≡ B C is replaced by (among other things) B C A. Even though these GCIs are absorbed, they still manifest as disjunctions and hence adversely affect the tableau reasoning process. 2 Alternately, a more optimal implementation is the following: instead of splitting the entire KB beforehand, we can perform a lazy splitting of certain specific axioms (on the fly) in order to improve the performance of the algorithm. The modified

algorithm with lazy splitting becomes:

• Given A unsatisfiable w.r.t T, find a single justification set, J ∈ JUST(A ≡ ⊥, T )

• Split axioms in J to give Js. Prune Js to arrive at a minimal precise justification set Jp In this case, it is possible to introduce a new absorption rule in the reasoner which would transform axioms of the form B A, C A, B C A to A ≡ B C internally. This obviously seems odd given that we split the KB initially and re-combine axioms back in the reasoner, but note that the goal here is finding precise justifications.

• Replace J by Js in T.

• Form Reiter’s HST using Jp as a node, with each outgoing edge being an axiom α ∈ Jp that is removed from T The advantage of this approach is that it only splits axioms in the intermediate justification sets in order to arrive at precise justifications, and re-inserts split axioms back into the KB dynamically. For details of the procedure, see [2] 5 Conclusion and Future Work We have implemented the axiom pinpointing service in the OWL-DL reasoner, Pellet, and exposed it in the OWL Ontology Editor, Swoop. We are in the process of extending it to capture precise justifications.

From a UI perspective, maintaining the correspondence between the subaxioms in the precise justification and the original asserted axioms is useful, as it allows us to strike out irrelevant parts of the axioms directly, which is helpful to understand the entailment better. (see Figure 5).

As future work, we plan to optimize the implementation and do a thorough performance and usability evaluation.

Figure 1: Justification for MaleStudentWith3Daughters Person in the Koala OWL Ontology References [1] Ian Horrocks and Ulrike Sattler. A tableaux decision procedure for SHOIQ. In Proc. of IJCAI 2005, 2005.

[2] Aditya Kalyanpur, Bijan Parsia, Bernardo Cuenca, and Evren Sirin. Axiom pinpointing: Finding (precise) justifications for arbitrary entailments in OWL-DL, 2006. Available at http://www.mindswap.org/papers/2006/AxiomPinpointing.pdf.

[3] Aditya Kalyanpur, Bijan Parsia, Evren Sirin, and James Hendler. Debugging unsatisfiable classes in OWL ontologies. J. of Web Semantics, Vol 3, Issue 4, 2005.

[4] S. Schlobach and R. Cornet. Non-standard reasoning services for the debugging

Similar works:

«REPORT OF THE NATIONAL YOUTH UNEMPLOYMENT SUMMIT With the Theme: “Empowering Youth Towards the Realisation of the Challenges of the Millennium Development Goals (MDGs)” Held on 27-29 August 2007, At the Pastoral Center Makurdi, Benue State, Nigeria. Organized by Pan African Civil society Network (PACSNET) Ngueinja Initiative of for Self Help and Development (NISHAD) Women's Right To Education Programme(WREP) YES Country Network Nigeria (YCNN) Justice Development and Peace Commission (JDPC),...»

«D000696 revision D CrystalTrak Application User’s Manual Rigaku Automation, Incorporated 5999 Avenida Encinas, Suite 150, Carlsbad, CA 92008 Phone: 760.438.5282 Fax: 760.438.5286 Web: www.rigaku.com/automation/index.html CrystalTrak, CrystalMation, Phoenix RE, Alchemist, Minstrel HT, Minstrel Desktop and CM View are trademarks of Rigaku Automation, TM TM TM TM TM TM TM Inc. All other trademarks and registered trademarks are the property of their respective owners. i © 2002-2008 Rigaku...»

«UNIVERSITY OF BELGRADE FACULTY OF ELECTRICAL ENGINEERING Yousef H. Abuadlla Flow-Based Anomaly Intrusion Detection System Using Two Neural Network Stages Doctoral Dissertation Belgrade, 2014 UNIVERZITET U BEOGRADU ELEKTROTEHNIČKI FAKULTET Yousef H. Abuadlla Sistem za detekciju upada zasnovan na tokovima sa dve neuralne mreže doktorska disertacija Beograd, 2014 Graduation committee: Chairman: Professor Zoran Jovanović School of Electrical Engineering, University of Belgrade Members: 1)...»

«Pragmatics 19:1.103-127 (2009) International Pragmatics Association TRANSLOCAL STYLE COMMUNITIES: HIP HOP YOUTH AS CULTURAL THEORISTS OF STYLE, LANGUAGE, AND GLOBALIZATION* H. Samy Alim Abstract This article addresses issues that lie at the intersection of debates about language, Hip Hop Culture, and globalization. Critically synthesizing a wide range of recent work on Hip Hop and foregrounding issues of youth agency as evidenced by Hip Hop youth’s metalinguistic theorizing, the article...»

«N Guía del usuario Ordenador Serie VPCC n2N Contenido Antes del uso Más información sobre el ordenador VAIO Consideraciones ergonómicas Uso de la red LAN inalámbrica Introducción Uso de la función BLUETOOTH Ubicación de los controles y los puertos Acerca de los indicadores luminosos Conexión de una fuente de alimentación Uso del paquete de batería Apagado seguro del ordenador Uso de los modos de ahorro de energía Mantenimiento del ordenador en condiciones ¿Cómo conectar un...»

«Dimarts, 14 de juny de 2016 ADMINISTRACIÓ LOCAL Ajuntament de Manresa ANUNCI El Ple de l'Ajuntament de Manresa, en sessió de data 19 de maig de 2016, va aprovar inicialment les Bases reguladores de les Ajudes a les empreses per a la contractació de persones aturades, en el marc del Programa complementari de foment de l'ocupació i de suport a la integració social de la Diputació de Barcelona. En compliment d'allò previst a l'article 124.2 del Decret 179/1995, de 13 de juny, pel qual...»

«HISTORY AND EVOLUTION OF THE TONADAS TRINITARIAS OF TRINIDAD DE CUBA By JOHNNY FRIAS A THESIS PRESENTED TO THE GRADUATE SCHOOL OF THE UNIVERSITY OF FLORIDA IN PARTIAL FULFILLMENT OF THE REQUIREMENTS FOR THE DEGREE OF MASTER OF MUSIC UNIVERSITY OF FLORIDA 2010 1 © 2010 Johnny Frías 2 To my great grandmother Flor Marina López, who introduced me to Cuban culture. 3 ACKNOWLEDGMENTS I would like to thank my parents and family, my good friend Pepe Clavijo, and my professors Larry Crook and Welson...»

«Essentials of Swedish Grammar: A Practical Guide to the Mastery of Swedish (Verbs and Essentials of Grammar Series) By Ake Viberg, Page: Intro & Details This compact volume offers an integrated guide to the major grammatical concepts needed for writing. From the Publisher COMPACT, CONVENIENT FORMAT. CONCISE, CLEAR EXPANATIONS OF A WIDE RANGE OF GRAMMAR POINTS. A CYCLICAL APPROACH TO THE PRESENTATION OF GRAMMAR POINTS, MEANING THAT ITEMS USUALLY PRESENTED ONLY ONCE IN GRAMMAR BOOKS ARE...»

«Research reactors in Russia. Status and prospects for reducing the fuel enrichment Valentin IVANOV Russian Academy of Sciences Washington, November 2010 The Russian Government mandated the ROSATOM to negotiate with the U.S. Department of Energy signing of an implementing agreement “concerning cooperation in research into feasibility of conversion of the Russian research reactors to use low enriched uranium fuel.” Related directive No 1919-r of October 30, 2010, was signed by Russian...»

«212 May 11, 2016 No. 198 IN THE COURT OF APPEALS OF THE STATE OF OREGON STATE OF OREGON, Plaintiff-Respondent, v. JAMES CHRISTOPHER HICKEY, Defendant-Appellant. Lane County Circuit Court 211218261; A153876 Ilisa Rooke-Ley, Judge. Argued and submitted April 21, 2015. Erica Herb, Deputy Public Defender, argued the cause for appellant. With her on the brief was Peter Gartlan, Chief Defender, Office of Public Defense Services. Joanna L. Jenkins, Assistant Attorney General, argued the cause for...»

«The Balitaan Newsletter is Published for the The Balitaan Newsletter is Published for the Filipino American Association of Portland Filipino American Association of Portland and the Vicinity, Inc. 8917the Vicinity, Inc. and SE Stark Street 8917 SE Stark Street Portland, Oregon 97216 Portland, Oregon 97216 WE WELCOME YOUR WE WELCOME YOUR COMMENTS AND SUGGESTIONS COMMENTS AND SUGGESTIONS If you would like to submit an idea, comments, Happy Spring & Lent Season to Everyone! If you would like to...»

«Subsurface Impacts of Hydraulic Fracturing: Contamination, Seismic Sensitivity, and Groundwater Use and Demand Management Published October, 2015 Prepared for: Canadian Water Network Prepared by: M. Cathryn Ryan (Principal Investigator), Daniel Alessi, Alireza Babaie Mahani, Aaron Cahill, John Cherry, David Eaton, Randal Evans, Naima Farah, Amélia Fernandes, Olenka Forde, Pauline Humez, Stefanie Kletke, Bethany Ladd, J.-M. Lemieux, Bernhard Mayer, K.U. Mayer, John Molson, Lucija Muehlenbachs,...»

<<  HOME   |    CONTACTS
2016 www.dissertation.xlibx.info - Dissertations, online materials

Materials of this site are available for review, all rights belong to their respective owners.
If you do not agree with the fact that your material is placed on this site, please, email us, we will within 1-2 business days delete him.