Tableau-based Reasoning for Description Logics with Inverse Roles and Number Restrictions Yu Ding A thesis submitted to the School of Graduate Studies in partial fulfilment of the requirements for the degree of Doctor of Philosophy Department of Computer Science & Software Engineering Concordia University April 2008 (cid:2)c Yu Ding, 2008 ABSTRACT Tableau-based Reasoning for Description Logics with Inverse Roles and Number Restrictions Yu Ding, Ph.D. Concordia University, 2008 The tableaux algorithm is a general technique for deciding concept satisfiability prob- lems in description logics (DLs). It is useful not only for practical implementations, but also for studying the correctness and complexity of concrete decision procedures. There is a family of DLs currently lack appropriate optimization techniques. The re- search focuses onthese DLswhich typically have inverse roles andnumber restrictions (corresponding to ontology languages OWL-lite and OWL-DL respectively). We pro- vide solutions to known problems such as the unsoundness of global tableaux caching, and present new tableau-based algorithms for concept satisfiability problems in these DLs. The research presented in this thesis is significant in several aspects. Firstly, based on an equivalence discovered during the course of the research, we are able to show an elimination of inverse roles for a sub-family of DLs. Our experiments have confirmed the practicality of this technique. Secondly, we provide three sub-tableaux caching techniques that is sound and global (but with different power in caching func- tionality). Finally, we present two ExpTime tableau-based decision procedures, with the one for SHIQ achieving an improved worst-case upper bound in the strong sense of binary coding of numbers (based on the integer linear programming technique). iii Contents Abstract iii List of Tables ix List of Figures x 1 Introduction 1 1.1 Background . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 1.2 Syntax and Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . 2 1.3 Tbox, Abox and Role Hierarchy . . . . . . . . . . . . . . . . . . . . . 7 1.3.1 Tbox . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 1.3.2 Abox . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 1.3.3 Role Hierarchy . . . . . . . . . . . . . . . . . . . . . . . . . . 10 1.4 Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 1.5 Research Motivation, Contribution and Report Organization . . . . . 14 1.5.1 Research Motivation . . . . . . . . . . . . . . . . . . . . . . . 14 1.5.2 Contributions . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 1.5.3 Report Organization . . . . . . . . . . . . . . . . . . . . . . . 17 iv 2 Dynamic Tableaux Caching for ALCI 20 2.1 The Tableaux Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 2.2 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 3 Inverse Role and ALCI Abox 31 3.1 An Equivalence on Inverse Relation . . . . . . . . . . . . . . . . . . . 31 3.2 Abox Consistency with Acyclic Tbox . . . . . . . . . . . . . . . . . . 33 3.2.1 The Intuition Behind the Conversion . . . . . . . . . . . . . . 33 3.2.2 The Three Steps . . . . . . . . . . . . . . . . . . . . . . . . . 37 3.2.3 Proofs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 3.3 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 4 A Tableaux Procedure for ALCFI 46 4.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 4.1.1 A Brief Review . . . . . . . . . . . . . . . . . . . . . . . . . . 46 4.1.2 Why Inverse Relation Is The Problem . . . . . . . . . . . . . . 48 4.1.3 A New Approach . . . . . . . . . . . . . . . . . . . . . . . . . 51 4.2 ALCFI Syntax and Semantics . . . . . . . . . . . . . . . . . . . . . 53 4.3 A Preprocessing Step . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 4.4 ALCFI Tableau Rules . . . . . . . . . . . . . . . . . . . . . . . . . . 56 4.5 ALCFI Decision Procedure . . . . . . . . . . . . . . . . . . . . . . . 59 4.5.1 The Procedure TEST(.,.) . . . . . . . . . . . . . . . . . . . . 59 4.5.2 The Procedure SAT(.,.,.,.) . . . . . . . . . . . . . . . . . . 61 4.5.3 The Sub-Procedure Successors(.,.,.) . . . . . . . . . . . . 62 4.5.4 The Sub-Procedure AllSuccessors(.,.) . . . . . . . . . . . 63 v 4.6 Equisatisfiability of the Preprocessing Step . . . . . . . . . . . . . . . 63 4.7 Correctness of the Decision Procedure . . . . . . . . . . . . . . . . . . 67 4.7.1 Completeness . . . . . . . . . . . . . . . . . . . . . . . . . . . 67 4.7.2 Soundness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 68 4.7.3 Complexity . . . . . . . . . . . . . . . . . . . . . . . . . . . . 72 4.8 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 73 5 SHOI, SHQ, and ALCHQI Acyclic Tbox 78 5.1 Reducing SHQ to ALCQ . . . . . . . . . . . . . . . . . . . . . . . . 78 5.2 Reducing SHOI to SHO . . . . . . . . . . . . . . . . . . . . . . . . 80 5.3 Reducing ALCHQI Acyclic Tbox . . . . . . . . . . . . . . . . . . . . 82 5.4 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 87 6 A Tableaux Procedure for SHIQ 88 6.1 Two Questions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 88 6.1.1 Big Number Values . . . . . . . . . . . . . . . . . . . . . . . . 88 6.1.2 Soundness of Tableaux Caching . . . . . . . . . . . . . . . . . 89 6.2 Syntax and Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . 90 6.3 The Algebraic Method for SHIQ . . . . . . . . . . . . . . . . . . . . 93 6.3.1 Fine-tuning on Modal Constraints . . . . . . . . . . . . . . . . 94 6.3.2 Atomic Decomposition and Integer Linear Program . . . . . . 95 6.3.3 A Concatenated Two-phase Decomposition . . . . . . . . . . . 98 6.3.4 Tableaux Structure . . . . . . . . . . . . . . . . . . . . . . . . 99 6.4 SHIQ Tableaux . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 100 6.4.1 Tableau Expansion Rules . . . . . . . . . . . . . . . . . . . . . 100 vi 6.4.2 Inconsistency Propagation Rules . . . . . . . . . . . . . . . . . 101 6.4.3 Blocking . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 102 6.5 SHIQ Algorithm . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 104 6.6 Proof . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 107 6.6.1 Completeness . . . . . . . . . . . . . . . . . . . . . . . . . . . 107 6.6.2 Soundness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 108 6.6.3 Complexity . . . . . . . . . . . . . . . . . . . . . . . . . . . . 111 6.7 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 114 6.7.1 Integer Linear Inequation . . . . . . . . . . . . . . . . . . . . 114 6.7.2 Atomic Decomposition . . . . . . . . . . . . . . . . . . . . . . 114 6.7.3 Reachability Analysis . . . . . . . . . . . . . . . . . . . . . . . 115 6.8 Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 116 6.9 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 118 7 Conclusion and Future Work 121 7.1 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 122 7.2 Conclusion and Future Research Direction . . . . . . . . . . . . . . . 125 Bibliography 127 A Tableau-based Decision Procedures and Optimizations 139 A.1 Tableau-based Decision Procedures . . . . . . . . . . . . . . . . . . . 139 A.2 General Optimizations . . . . . . . . . . . . . . . . . . . . . . . . . . 142 A.2.1 Concept Unfolding . . . . . . . . . . . . . . . . . . . . . . . . 143 A.2.2 Normalization and Simplification . . . . . . . . . . . . . . . . 145 vii A.2.3 Internalization . . . . . . . . . . . . . . . . . . . . . . . . . . . 146 A.2.4 Branching . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 147 A.2.5 Backtracking . . . . . . . . . . . . . . . . . . . . . . . . . . . 148 A.2.6 Axiom Transformation . . . . . . . . . . . . . . . . . . . . . . 149 A.2.7 Blocking . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 150 A.2.8 Caching Technique . . . . . . . . . . . . . . . . . . . . . . . . 151 A.3 Reasoning About Inverse Roles . . . . . . . . . . . . . . . . . . . . . 154 A.4 Reasoning About Number Restrictions . . . . . . . . . . . . . . . . . 156 B Empirical Results 158 viii List of Tables 2.1 Tableau rules for ALCI with an integrated generalized cache. . . . . 25 4.1 The tableaux expansion rules for ALCFI. . . . . . . . . . . . . . . . 57 4.2 The inconsistency propagation rule for ALCFI. . . . . . . . . . . . . 59 6.1 The tableau expansion rules for SHIQ. . . . . . . . . . . . . . . . . 100 6.2 The inconsistency propagation rule for SHIQ. . . . . . . . . . . . . . 101 B.1 Experimental results (all times are given in seconds) . . . . . . . . . . 159 ix List of Figures 1.1 Description Logics and Their Language Elements . . . . . . . . . . . 6 1.2 A Pictorial Presentation of (Partial) Knowledge of the Examples . . . 12 1.3 Organization of the Chapters and Appendices . . . . . . . . . . . . . 19 2.1 Dynamic Caching: Condition 1 . . . . . . . . . . . . . . . . . . . . . 27 2.2 Dynamic Caching: Condition 2 . . . . . . . . . . . . . . . . . . . . . 27 2.3 Dynamic Caching: Condition 3 . . . . . . . . . . . . . . . . . . . . . 28 2.4 Dynamic Caching: Condition 4 . . . . . . . . . . . . . . . . . . . . . 29 3.1 The Syntax Tree of Concept Expressions . . . . . . . . . . . . . . . . 34 3.2 The Role Assertions In Abox . . . . . . . . . . . . . . . . . . . . . . . 35 3.3 The Role Assertions In Abox After Polarisation . . . . . . . . . . . . 36 3.4 Backward Constraint Propagation . . . . . . . . . . . . . . . . . . . . 39 3.5 An Example Abox . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 4.1 Inconsistency Propagation and Backward Constraint Propagation . . 48 4.2 A Model for ¬A w.r.t. T = {(cid:3) (cid:4) (≤ R−),(cid:3) (cid:4) ∃R.A} . . . . . . . . 49 1 4.3 Blocking and Unravelling . . . . . . . . . . . . . . . . . . . . . . . . . 70 5.1 The Modal-reference Relation of an Imaginary Acyclic Tbox . . . . . 83 x