|
|
Bernardo Cuenca-Grau, Ian Horrocks, Yevgeny Kazakov, and Ulrike Sattler.
Modular Reuse of Ontologies: Theory and Practice.
JAIR, 31:273-318, 2008.
[ BibTeX-Entry |
URL |
Pdf (605K) ]
In this paper, we propose a set of tasks that are
relevant for the modular reuse of ontologies. In
order to formalize these tasks as reasoning
problems, we introduce the notions of conservative
extension, safety and module for a very general
class of logic-based ontology languages. We
investigate the general properties of and
relationships between these notions and study the
relationships between the relevant reasoning
problems we have previously identified. To study the
computability of these problems, we consider, in
particular, Description Logics (DLs), which provide
the formal underpinning of the W3C Web Ontology
Language (OWL), and show that all the problems we
consider are undecidable or algorithmically
unsolvable for the description logic underlying OWL
DL. In order to achieve a practical solution, we
identify conditions sufficient for an ontology to
reuse a set of symbols “safely”-that is, without
changing their meaning. We provide the notion of a
safety class, which characterizes any sufficient
condition for safety, and identify a family of
safety classes-called locality-which enjoys a
collection of desirable properties. We use the
notion of a safety class to extract modules from
ontologies, and we provide various modularization
algorithms that are appropriate to the properties of
the particular safety class in use. Finally, we show
practical benefits of our safety checking and module
extraction algorithms.
Bernardo Cuenca-Grau, Ian Horrocks, Yevgeny Kazakov, and Ulrike Sattler.
Ontology Reuse: Better Safe than Sorry.
In Description Logics, pages 41-52, Brixen/Bressanone, Italy,
June 8-10 2007. Bozen/Bolzano University Press.
[ BibTeX-Entry |
URL |
Pdf (181K) ]
Bernardo Cuenca-Grau, Ian Horrocks, Yevgeny Kazakov, and Ulrike Sattler.
Extracting Modules From Ontologies: A Logic-based
Approach.
In OWL: Experiences and Directions 2007 (OWLED 2007),
Innsbruck, Austria, June 6-7 2007.
[ BibTeX-Entry |
URL |
Pdf (168K) ]
Bernardo Cuenca-Grau, Ian Horrocks, Yevgeny Kazakov, and Ulrike Sattler.
Just the Right Amount: Extracting Modules from
Ontologies.
In WWW, pages 717-726, Banff, Canada, May 2007. ACM.
[ BibTeX-Entry |
URL |
Pdf (379K) ]
The ability to extract meaningful fragments from an ontology is essential for ontology re-use. We propose a definition of a module that guarantees to completely capture the meaning of a given set of terms, i.e., to include all axioms relevant to the meaning of these terms, and study the problem of extracting minimally sized modules. We show that the problem of determining whether a subset of an ontology is a module for a given vocabulary is undecidable even for rather restricted sub-languages of OWL DL. Hence we propose two approximations, i.e., alternative definitions of modules for a vocabulary that still provide the above guarantee, but that are possibly too strict, and that may thus result in larger modules: the first approximation is semantic and can be checked using existing DL reasoners; the second is syntactic, and can be computed in polynomial time. Finally, we report on an empirical evaluation of our syntactic approximation that demonstrates that the modules we extract are surprisingly small.
Yevgeny Kazakov, Ulrike Sattler, and Evgeny Zolin.
How Many Legs Do I Have? Non-Simple Roles in Number
Restrictions Revisited.
In LPAR, volume 4790 of Lecture Notes in Computer
Science, pages 303-317. Springer, 2007.
[ BibTeX-Entry |
Pdf (265K) ]
The Description Logics underpinning OWL impose a well-known syntactic restriction in order to preserve decidability: they do not allow to use non-simple roles-that is, transitive roles or their super-roles-in number restrictions. When modeling composite objects, for example in bio-medical ontologies, this restriction can pose problems. Therefore, we take a closer look at the problem of counting over non-simple roles. On the one hand, we sharpen the known undecidability results and demon-strate that: (i) for DLs with inverse roles, counting over non-simple roles leads to undecidability even when there is only one role in the language; (ii) for DLs without inverses, two transitive and an arbitrary role are sufficient for undecidability. On the other hand, we demonstrate that counting over non-simple roles does not compromise decidability in the absence of inverse roles provided that certain restrictions on role inclusion axioms are satisfied
Bernardo Cuenca-Grau, Christian Halaschek-Wiener, and Yevgeny Kazakov.
History Matters: Incremental Ontology Reasoning Using
Modules.
In ISWC/ASWC, volume 4825 of Lecture Notes in Computer
Science, pages 183-196. Springer, 2007.
[ BibTeX-Entry |
Pdf (207K) ]
The development of ontologies involves continuous but relatively small modifications. Existing ontology reasoners, however, do not take advantage of the similarities between different versions of an ontology. In this paper, we propose a technique for incremental reasoning-that is, reasoning that reuses information obtained from previous versions of an ontology-based on the notion of a module. Our technique does not depend on a particular reasoning calculus and thus can be used in combination with any reasoner. We have applied our results to incremental classification of OWL DL ontologies and found significant improvement over regular classification time on a set of real-world ontologies.
Bernardo Cuenca-Grau, Ian Horrocks, Yevgeny Kazakov, and Ulrike Sattler.
A Logical Framework for Modularity of Ontologies.
In IJCAI, pages 298-303, 2007.
[ BibTeX-Entry |
Pdf |
Pdf (131K) ]
Modularity is a key requirement for collaborative ontology engineering and for distributed ontology reuse on the Web. Modern ontology languages, such as OWL, are logic-based, and thus a useful notion of modularity needs to take the semantics of
ontologies and their implications into account. We propose a logic-based notion of modularity that allows the modeler to specify the external signature of their ontology, whose symbols are assumed to be defined in some other ontology. We define two
restrictions on the usage of the external signature, a syntactic and a slightly less restrictive, semantic one, each of which is decidable and guarantees a certain kind of black-box behavior, which enables the controlled merging of ontologies. Analysis of real-world ontologies suggests that these restrictions are not too onerous.
Yevgeny Kazakov and Boris Motik.
A Resolution-Based Decision Procedure for SHOIQ.
In IJCAR, volume 4130 of Lecture Notes in Computer
Science, pages 662-677. Springer, 2006.
[ BibTeX-Entry |
URL |
Pdf (230K) ]
We present a resolution-based decision procedure for the description logic SHOIQ-the logic underlying the Semantic Web ontology language OWLDL. Our procedure is goal-oriented, and it naturally extends a similar procedure for SHIQ, which has proven itself in practice. Applying existing techniques for saturation-based decision procedures to SHOIQ is not straightforward due to nominals, number restrictions, and inverse roles-a combination known to cause termination problems. We overcome this difficulty by using the basic superposition calculus, extended with custom simplification rules.
Yevgeny Kazakov.
A Polynomial Translation from the Two-Variable Guarded
Fragment with Number Restrictions to the Guarded Fragment.
In JELIA, volume 3229 of Lecture Notes in Computer
Science, pages 372-384. Springer, 2004.
[ BibTeX-Entry |
URL |
PostScript [g-zip'd] (108K) |
Pdf (202K) ]
We consider a two-variable guarded fragment with number restrictions for binary relations and give a satisfiability
preserving transformation of formulas in this fragment to the three-variable guarded fragment. The translation can be computed in polynomial time and produces a formula that is linear in the size of the initial formula even for the binary coding of number restrictions. This allows one to reduce reasoning problems for many description logics to the satisfiability problem for the guarded fragment
Yevgeny Kazakov and Hans de Nivelle.
A Resolution Decision Procedure for the Guarded Fragment
with Transitive Guards.
In IJCAR, volume 3097 of Lecture Notes in Computer
Science, pages 122-136. Springer, 2004.
[ BibTeX-Entry |
URL |
PostScript [g-zip'd] (97K) |
Pdf (224K) ]
We show how well-known refinements of ordered resolution, in particular redundancy elimination and ordering constraints in combination with a selection function, can be used to obtain a decision procedure for the guarded fragment with transitive guards. Another contribution of the paper is a special scheme notation, that allows to describe saturation strategies and show their correctness in a concise form
Yevgeny Kazakov.
A Resolution Decision Procedure for the Guarded Fragment
with Transitive Guards.
In IJCAR Doctoral Programme, volume 106 of CEUR Workshop
Proceedings, 2004.
[ BibTeX-Entry ]
We show how well-known refinements of ordered resolution, in particular redundancy elimination and ordering constraints in combination with a selection function, can be used to obtain a decision procedure for the guarded fragment with transitive guards. Another contribution of the paper is a special scheme notation, that allows to describe saturation strategies and show their correctness in a concise form
Yevgeny Kazakov and Hans de Nivelle.
Subsumption of Concepts in FL0 for (Cyclic)
Terminologies with Respect to Descriptive Semantics is PSPACE-complete.
In Description Logics, volume 81 of CEUR Workshop
Proceedings, 2003.
[ BibTeX-Entry |
PostScript [g-zip'd] (83K) |
Pdf (153K) ]
We close the gap in the complexity classification of subsumption in the simple description logic FL0, which allows for conjunctions and universal value restriction only. We prove that the subsumption problem in FL0 is PSPACE-complete for descriptive semantics when cyclic definitions are allowed. Our proof uses automata theory and as a by-product we establish the PSPACE-completeness of a certain decision problem for regular languages
Yevgeny Kazakov.
Recursive resolution for modal logic.
In Proceedings of the Symposium on the Effectiveness of Logic in
Computer Science in Honour of Moshe Vardi, volume MPI-I-2002-2-007 of
MPI Research Report, pages 11-15, Saarbrücken, Germany, March 2002.
International Max Planck Research School for Computer Science (IMPRS),
Max-Planck-Institut für Informatik.
[ BibTeX-Entry |
PostScript [g-zip'd] (47K) ]
Resolution for the first order logic can be considered as a practical tool for obtaining a decision procedures for some theories (cf. [?]). For modal logics, however, there is no uniform formulation of the resolution principle, yet the normal modal logics are the most probable candidates to be decidable theories. The translational methods for modal logic, treated for instance in [?], yet possess some uniformness property, but does not let one to extract proofs from the refutations. On the other hand, direct methods (cf. [?], [?]) are local which gives not much practical use of them. This paper presents some arguments on generalization of the classical propositional resolution method to the language of modal logic. We give a resolution calculus for modal logic that inherits some features of classical resolution and propose some suggestions of how can it be used for other modal logics
Yevgeny Kazakov, Ulrike Sattler, and Evgeny Zolin.
Is Your RBox Safe?
Research report, The University of Manchester, Oxford Road,
Manchester M13 9PL, UK, July 2007.
[ BibTeX-Entry |
Pdf (361K) ]
The Description Logics underpinning OWL impose a well-known syntactic restriction in order to preserve decidability: they do not allow to use non-simple roles-that is, transitive roles or their super-roles-in number restrictions. When modeling composite objects, for example in bio-medical ontologies, this restriction can pose problems. Therefore, we take a closer look at the problem of counting over non-simple roles. On the one hand, we sharpen the known undecidability results and demonstrate that: (i) for DLs with inverse roles, counting over non-simple roles leads to undecidability even when there is only one role in the language; (ii) for DLs without inverses, two transitive and an arbitrary role are sufficient for undecidability. On the other hand, we demonstrate that counting over non-simple roles does not compromise decidability in the absence of inverse roles provided that certain restrictions on role inclusion axioms are satisfied.
Bernardo Cuenca-Grau, Ian Horrocks, Yevgeny Kazakov, and Ulrike Sattler.
Extracting Modules from Ontologies: Theory and
Practice.
Research report, The University of Manchester, Oxford Road,
Manchester M13 9PL, UK, February 2007.
[ BibTeX-Entry |
Pdf (329K) ]
The ability to extract meaningful fragments from an ontology is essential for ontology re-use. We propose a definition of a module that guarantees to completely capture the meaning of a given set of terms, i.e., to include all axioms relevant to the meaning of these terms, and study the problem of extracting minimally sized modules. We show that the problem of determining whether a subset of an ontology is a module for a given vocabulary is undecidable even for rather restricted sub-languages of OWL DL. Hence we propose two approximations, i.e., alternative definitions of modules for a vocabulary that still provide the above guarantee, but that are possibly too strict, and that may thus result in larger modules: the first approximation is semantic and can be checked using existing DL reasoners; the second is syntactic, and can be computed in polynomial time. Finally, we report on an empirical evaluation of our syntactic approximation that demonstrates that the modules we extract are surprisingly small.
Yevgeny Kazakov and Hans de Nivelle.
Resolution Decision Procedures for the Guarded Fragment
with Transitive Guards.
Research Report MPI-I-2004-2-001, Max-Planck-Institut für
Informatik, Stuhlsatzenhausweg 85, 66123 Saarbrücken, Germany, April
2004.
[ BibTeX-Entry |
PostScript [g-zip'd] (248K) |
Pdf (269K) ]
We show how well-known refinements of ordered resolution, in particular redundancy elimination and ordering constraints in combination with a selection function, can be used to obtain a decision procedure for the guarded fragment with transitive guards. Another contribution of the paper is a special scheme notation, that allows to describe saturation strategies and show their correctness in a concise form
Yevgeny Kazakov and Hans de Nivelle.
Subsumption of concepts in DL FL0 for
(cyclic) terminologies with respect to descriptive semantics is
PSPACE-complete.
Research Report MPI-I-2003-2-003, Max-Planck-Institut für
Informatik, Stuhlsatzenhausweg 85, 66123 Saarbrücken, Germany, April
2003.
[ BibTeX-Entry |
PostScript [g-zip'd] (137K) |
Pdf (133K) ]
We prove the PSPACE-completeness of the subsumption problem for(cyclic) terminologies with respect to descriptive semantics in a simple Description Logic FL0, which allows for conjunctions and universal value restrictions only, thus solving the problem which was open for more than ten years
S. Artemov, E. Kazakov, and D. Shapiro.
On logic of knowledge with justifications.
Technical Report CFIS 99-12, Cornell University, 1999.
[ BibTeX-Entry |
PostScript [g-zip'd] (64K) ]
Yevgeny Kazakov.
SRIQ and SROIQ are Harder than SHOIQ.
submitted, 2008.
[ BibTeX-Entry |
Pdf (365K) ]
Yevgeny Kazakov and Boris Motik.
A Resolution-Based Decision Procedure for SHOIQ.
To appear, 2008.
[ BibTeX-Entry |
Pdf (321K) ]
We present a resolution-based decision procedure for the description logic SHOIQ-the logic underlying the Semantic Web ontology language OWL-DL. Our procedure is goal-oriented, and it naturally extends a similar procedure for SHIQ, which has proven itself in practice. Extending this procedure to SHOIQ using existing techniques is not straightforward because of nominals, number restrictions, and inverse roles-a combination known to cause termination problems. We overcome this difficulty by using basic superposition calculus extended with custom simplification rules.
Yevgeny Kazakov.
A Framework of Refutational Theorem Proving for
Saturation-Based Decision Procedures.
Research Report MPI-I-2005-2-004, Max-Planck-Institut für
Informatik, on revison, August 2005.
[ BibTeX-Entry |
Pdf (1M) ]
Automated state-of-the-art theorem provers are typically optimised for particular strategies, and there are only limited number of options that can be set by the user. Probably because of this, the general conditions on applicability of saturation-based calculi have not been thoroughly investigated. However for some applications, e.g., for saturation-based decision procedures, one would like to have more options in order to design flexible saturation strategies.
In this report we revisit several well-known saturation-based calculi used in automated deduction: Ordered Resolution, Ordered Paramodulation, Superposition and Chaining calculi. We give a uniform account on completeness proofs for these calculi using the standard model construction procedures of Bachmair and Ganzinger. By careful inspection of these proofs, we formulate some variations of inference rules and general conditions on orderings under which the calculi remain refutationally complete. In particular, we considerably generalise the known class of admissible orderings for the Chaining calculi.
We also consider in details the standard notion of redundancy, estimate the complexity for the steps of the clause normal form transformation, and
give a computational model of the saturation process.
Yevgeny Kazakov.
Combining Resolution Decision Procedures.
unpublished manuscript, available from
http://web.comlab.ox.ac.uk/oucl/work/yevgeny.kazakov/publications/,
2004.
[ BibTeX-Entry |
PostScript [g-zip'd] (118K) |
Pdf (253K) ]
We present resolution-based decision procedures for the guarded, two-variable and monadic fragments without equality in a uniform way and show how they can be combined. In this way, new decidable fragments are obtained. We make use of a novel technique for describing resolution decision procedures by means of clause schemes. The scheme notation provides a convenient way of specifying decision procedures, proving their correctness and analyzing complexity of associated decision problems. We also show that many decidability results obtained in the paper cannot be extended to the case with equality
Yevgeny Kazakov.
Saturation-Based Decision Procedures for Extensions of the
Guarded Fragment.
PhD thesis, Universität des Saarlandes, Saarbrücken, Germany,
March 2006.
[ BibTeX-Entry |
Pdf (2M) ]
We apply the framework of Bachmair and Ganzinger for saturation-based theorem proving to derive a range of decision procedures for logical formalisms, starting with a simple terminological language EL, which allows for conjunction and existential restrictions only, and ending with extensions of the guarded fragment with equality, constants, functionality, number restrictions and compositional axioms of form SoT< H. Our procedures are derived in a uniform way using standard saturation-based calculi enhanced with simplification rules based on the general notion of redundancy. We argue that such decision procedures can be applied for reasoning in description logics, where they have certain advantages over traditionally used tableau procedures, such as optimal worst-case complexity and direct correctness proofs
|
|
|
|
