product iamge

Consequence Finding in Modal Logic [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): Meghyn Bienvenu
Publisher: Toulouse University
Year: 2009

Language: English
Pages: 214

1 Introduction 1
2 The Modal Logic Kn 11
2.1 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
2.2 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
2.3 Logical Consequence . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
2.4 Basic Transformations . . . . . . . . . . . . . . . . . . . . . . . . . . 20
2.5 Basic Reasoning Tasks . . . . . . . . . . . . . . . . . . . . . . . . . . 27
2.6 Uniform Interpolation . . . . . . . . . . . . . . . . . . . . . . . . . . 33
2.7 Relation to First-Order Logic . . . . . . . . . . . . . . . . . . . . . . 41
2.8 Relation to Description Logics . . . . . . . . . . . . . . . . . . . . . . 42
2.8.1 A short introduction to description logics . . . . . . . . . . . 43
2.8.2 The description logic ALC . . . . . . . . . . . . . . . . . . . . 44
2.8.3 The description logic ALE . . . . . . . . . . . . . . . . . . . . 46
3 Prime Implicates and Prime Implicants in Kn 51
3.1 Defining Clauses and Terms in Kn . . . . . . . . . . . . . . . . . . . 51
3.1.1 Impossibility result . . . . . . . . . . . . . . . . . . . . . . . . 52
3.1.2 Analysis of candidate definitions . . . . . . . . . . . . . . . . 54
3.1.3 Summary and discussion . . . . . . . . . . . . . . . . . . . . . 66
3.2 Defining Prime Implicates and Prime Implicants in Kn . . . . . . . . 67
3.2.1 Basic definitions . . . . . . . . . . . . . . . . . . . . . . . . . 67
3.2.2 Desirable properties . . . . . . . . . . . . . . . . . . . . . . . 68
3.2.3 Analysis of candidate definitions . . . . . . . . . . . . . . . . 69
4 Generating and Recognizing Prime Implicates 79
4.1 Prime Implicate Generation . . . . . . . . . . . . . . . . . . . . . . . 79
4.1.1 Prime implicate generation in propositional logic . . . . . . . 79
4.1.2 The algorithm GenPI . . . . . . . . . . . . . . . . . . . . . . 80
4.1.3 Correctness of GenPI . . . . . . . . . . . . . . . . . . . . . . 82
4.1.4 Bounds on prime implicate size . . . . . . . . . . . . . . . . . 85
4.1.5 Bounds on the number of prime implicates . . . . . . . . . . 92
4.1.6 Improving the efficiency of GenPI . . . . . . . . . . . . . . . 95
4.2 Prime Implicate Recognition . . . . . . . . . . . . . . . . . . . . . . 100
4.2.1 Lower bound . . . . . . . . . . . . . . . . . . . . . . . . . . . 100
4.2.2 Na¨ıve approach . . . . . . . . . . . . . . . . . . . . . . . . . . 100
4.2.3 Decomposition theorem . . . . . . . . . . . . . . . . . . . . . 101
4.2.4 Prime implicate recognition for propositional clauses . . . . . 106
4.2.5 Prime implicate recognition for 2-formulae . . . . . . . . . . 107
4.2.6 Prime implicate recognition for 3-formulae . . . . . . . . . . 108
4.2.7 The algorithm TestPI . . . . . . . . . . . . . . . . . . . . . . 113
5 Restricted Consequence Finding 119
5.1 New prime implicates . . . . . . . . . . . . . . . . . . . . . . . . . . 119
5.1.1 Properties of new prime implicates . . . . . . . . . . . . . . . 120
5.1.2 Generating and recognizing new prime implicates . . . . . . . 122
5.2 Signature-bounded prime implicates . . . . . . . . . . . . . . . . . . 123
5.2.1 Properties of signature-bounded prime implicates . . . . . . . 124
5.2.2 Generating signature-bounded prime implicates . . . . . . . . 128
5.2.3 Recognizing signature-bounded prime implicates . . . . . . . 128
6 Prime Implicate Normal Form 131
6.1 Motivation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 131
6.2 Definition of Prime Implicate Normal Form . . . . . . . . . . . . . . 132
6.3 Properties of Prime Implicate Normal Form . . . . . . . . . . . . . . 135
6.3.1 Tractable entailment . . . . . . . . . . . . . . . . . . . . . . . 135
6.3.2 Tractable uniform interpolation . . . . . . . . . . . . . . . . . 153
6.3.3 Canonicity . . . . . . . . . . . . . . . . . . . . . . . . . . . . 167
6.4 Computing Prime Implicate Normal Form . . . . . . . . . . . . . . . 170
6.5 Spatial Complexity of Prime Implicate Normal Form . . . . . . . . . 173
6.6 Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 177
6.6.1 Disjunctive form . . . . . . . . . . . . . . . . . . . . . . . . . 177
6.6.2 Linkless normal form . . . . . . . . . . . . . . . . . . . . . . . 179
7 Conclusion 183
A Complexity Theory 187
Bibliography 189
Index 197