A proof theory for description logics

Cover......Page 1
A Proof Theory for 
Description Logics......Page 3
Preface......Page 6
Contents......Page 7
9 Conclusion......Page 9
1.2 Motivation......Page 10
1.4 How This Book is Organized......Page 12
References......Page 13
2.1 A Basic Description Logic......Page 16
2.2 Individuals......Page 18
2.3 Description Logics Family......Page 19
2.5 Inference Algorithms......Page 20
2.6 cal Axiomatization......Page 21
References......Page 22
3.1 A Sequent Calculus for cal......Page 23
3.2 cal Soundness......Page 26
3.3 The Completeness of cal......Page 30
3.4 The Cut-Elimination Theorem......Page 31
References......Page 42
4.1 Introduction......Page 43
4.3 Obtaining Counter-Models From Unsuccessful  Proof Trees......Page 44
Reference......Page 55
5.1 Introduction......Page 56
5.2 The cal System......Page 57
5.3 cal Soundness......Page 58
5.4 cal Completeness......Page 61
5.5 Normalization Theorem for cal......Page 62
References......Page 68
6.2 cal Introduction......Page 69
6.3 The Sequent Calculus for cal......Page 70
6.4 cal Soundness......Page 73
6.5 On cal Completeness......Page 76
6.7 cal Soundness......Page 77
References......Page 79
7.1 Introduction......Page 80
7.2 An Example of Explanations From Proofs  in cal......Page 85
7.3 Explaining UML in cal......Page 86
References......Page 88
8.1 Overview of the Maude System......Page 90
8.2.1 The Logical Language......Page 92
8.2.2 The Sequent Calculus......Page 94
8.3 The cal System......Page 96
8.3.1 The cal System Implementation......Page 97
8.3.2 The Interface......Page 99
8.3.3 Defining Proof Strategies......Page 102
References......Page 105
9.1 Contributions......Page 106
References......Page 108