product iamge

Complexity Results and Practical Algorithms for Logics in Knowledge Representation [PhD Thesis]

This document was uploaded by one of our users. The uploader already confirmed that they had the permission to publish it. If you are author/publisher or own the copyright of this documents, please report to us by using this DMCA report form.

Download
Search on Amazon

Simply click on the Download Book button.

Yes, Book downloads on Ebookily are 100% Free.

Sometimes the book is free on Amazon As well, so go ahead and hit "Search on Amazon"

Author(s): Stephan Tobies
Publisher: Technische Hochschule Aachen
Year: 2001

Language: English
Pages: 182

1 Introduction 1
1.1 Description Logic Systems . . . . . . . . . . . . . . . . . . . . . . . . . . . 1
1.2 Reasoning in Description Logics . . . . . . . . . . . . . . . . . . . . . . . . 3
1.3 Expressive Description Logics . . . . . . . . . . . . . . . . . . . . . . . . . 3
1.3.1 Counting . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4
1.3.2 Transitive Roles, Role Hierarchies, and Inverse Roles . . . . . . . . 4
1.3.3 Nominals . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5
1.4 Guarded Logics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6
1.5 Outline and Structure of this Thesis . . . . . . . . . . . . . . . . . . . . . . 7
2 Preliminaries 11
2.1 The Basic DL ALC . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
2.2 Terminological and Assertional Formalism . . . . . . . . . . . . . . . . . . 13
2.3 Inference Problems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14
3 Reasoning in Description Logics 17
3.1 Reasoning Paradigms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
3.2 Tableau Reasoning for ALC-satis ability . . . . . . . . . . . . . . . . . . . 20
3.2.1 Deciding Concept Satis ability for ALC . . . . . . . . . . . . . . . . 21
3.2.2 Complexity . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
3.2.3 Other Inference Problems for ALC . . . . . . . . . . . . . . . . . . . 31
4 Qualifying Number Restrictions 35
4.1 Syntax and Semantics of ALCQ . . . . . . . . . . . . . . . . . . . . . . . . 36
4.2 Counting Pitfalls . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
4.2.1 An Incorrect Solution . . . . . . . . . . . . . . . . . . . . . . . . . . 37
4.2.2 A Correct but Inecient Solution . . . . . . . . . . . . . . . . . . . 40
4.3 An Optimal Solution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
4.3.1 Correctness of the Optimized Algorithm . . . . . . . . . . . . . . . 42
4.3.2 Complexity of the Optimal Algorithm . . . . . . . . . . . . . . . . . 47
4.4 Extensions of ALCQ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
4.4.1 Reasoning for ALCQIb . . . . . . . . . . . . . . . . . . . . . . . . . . 51
4.4.2 Correctness of the Algorithm . . . . . . . . . . . . . . . . . . . . . 54
4.4.3 Complexity of the Algorithm . . . . . . . . . . . . . . . . . . . . . . 59
4.5 Reasoning with ALCQIb-Knowledge Bases . . . . . . . . . . . . . . . . . . . 61
5 Cardinality Restrictions and Nominals 75
5.1 Syntax and Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 76
5.2 The Complexity of Cardinality Restrictions and Nominals . . . . . . . . . 78
5.2.1 Cardinality Restrictions and ALCQI . . . . . . . . . . . . . . . . . . 79
5.2.2 Boolean Role Expressions . . . . . . . . . . . . . . . . . . . . . . . 89
6 Transitive Roles and Role Hierarchies 93
6.1 Transitive and Inverse Roles: SI . . . . . . . . . . . . . . . . . . . . . . . . 94
6.1.1 The SI-algorithm . . . . . . . . . . . . . . . . . . . . . . . . . . . . 95
6.1.2 Blocking . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 96
6.1.3 A Tableau Algorithm for SI . . . . . . . . . . . . . . . . . . . . . . 100
6.1.4 Constructing an SI Tableau . . . . . . . . . . . . . . . . . . . . . . 102
6.1.5 Complexity . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 109
6.2 Adding Role Hierarchies and Qualifying Number Restrictions: SHIQ . . . 112
6.2.1 Syntax and Semantics . . . . . . . . . . . . . . . . . . . . . . . . . 113
6.2.2 The Complexity of Reasoning with SHIQ . . . . . . . . . . . . . . . 115
6.3 Practical Reasoning for SHIQ . . . . . . . . . . . . . . . . . . . . . . . . . 121
6.3.1 A SHIQ-Tableau . . . . . . . . . . . . . . . . . . . . . . . . . . . . 122
6.3.2 A Tableau Algorithm for SHIQ . . . . . . . . . . . . . . . . . . . . 124
7 Guarded Fragments 137
7.1 Syntax and Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 138
7.2 Reasoning with Guarded Fragments . . . . . . . . . . . . . . . . . . . . . . 140
7.2.1 Tableau Reasoning for CGF . . . . . . . . . . . . . . . . . . . . . . 141
7.2.2 Correctness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 144
8 Summary 155
Bibliography 159
List of Figures 173