Knowledge in Action: Logical Foundations for Specifying and Implementing Dynamical Systems

Contents......Page 8
Preface......Page 18
Acknowledgments......Page 20
1 Introduction......Page 22
2.1.1 Syntax......Page 26
2.1.2 Semantics......Page 27
2.1.4 Many-Sorted First-Order Languages......Page 29
2.1.7 A Limitation of First-Order Logic......Page 31
2.2.2 Semantics......Page 33
2.2.3 Inductive Definitions and Second-Order Logic......Page 34
2.3 Exercises......Page 36
2.4 Bibliographic Remarks......Page 39
3.1.1 Intuitive Ontology for the Situation Calculus......Page 40
3.1.3 The Qualification Problem for Actions......Page 41
3.1.4 The Frame Problem......Page 43
3.2 A Simple Solution to the Frame Problem (Sometimes)......Page 44
3.2.1 Frame Axioms: Pednault’s Proposal......Page 45
3.2.2 Frame Axioms: The Davis/Haas/Schubert Proposal......Page 47
3.2.3 A Simple Solution (Sometimes)......Page 49
3.2.4 Aside: Normal Forms for Effect Axioms......Page 50
3.2.5 A Simple Solution: The General Case......Page 51
3.2.6 A Simple Solution: Functional Fluents......Page 53
3.2.7 A Simple Solution: Summary......Page 55
3.3 Deductive Planning with the Situation Calculus......Page 56
3.4.3 The Basic Approach: An Example......Page 60
3.5 Exercises......Page 62
3.6 Bibliographic Remarks......Page 65
4.1 The Language of the Situation Calculus......Page 68
4.2.1 Number Theory......Page 69
4.2.2 Foundational Axioms for Situations......Page 70
4.2.4 Executable Situations......Page 73
4.2.5 Further Consequences of the Foundational Axioms......Page 74
4.3 Reasoning about Situations Using Induction......Page 75
4.3.1 Some Examples of Inductive Proofs......Page 76
4.3.2 State Constraints......Page 78
4.4 Basic Theories of Action......Page 79
4.5 Regression......Page 82
4.6.1 Executable Ground Action Sequences......Page 88
4.6.2 The Projection Problem and Query Evaluation......Page 90
4.7 Regression with Functional Fluents......Page 91
4.8 Database Logs and Historical Queries......Page 94
4.8.1 Querying All Past Situations......Page 95
4.8.2 Querying Some Past Situation......Page 97
4.8.3 The Projection Problem Revisited......Page 98
4.9 Exercises......Page 99
4.10 Bibliographic Remarks......Page 104
5.1 Logical Foundations of Prolog......Page 106
5.1.1 Why Insist on a Proper Prolog Interpreter?......Page 108
5.1.2 More on the Equational Theory of Clark’s Theorem......Page 109
5.2 Lloyd-Topor Normal Forms for Arbitrary Definitions and Goals......Page 111
5.2.1 What Are the Lloyd-Topor Auxiliary Predicates?......Page 112
5.2.2 Accommodating Arbitrary Goals......Page 113
5.2.3 Definitional Theories: Soundness, Completeness, and Closed Worlds......Page 115
5.3 Basic Action Theories, Definitions, and Regressable Queries......Page 116
5.3.2 Definitional Form for Successor State Axioms......Page 117
5.3.4 Revised Lloyd-Topor Transformations......Page 123
5.4 Exercises......Page 128
5.5 Bibliographic Remarks......Page 129
6.1 Complex Actions and Procedures in the Situation Calculus......Page 132
6.1.1 Procedures......Page 135
6.1.2 Programs and Executable Situations......Page 137
6.1.3 Why Macros?......Page 138
6.1.4 Programs as Macros: What Price Must Be Paid?......Page 139
6.2 An Elevator Controller in Golog......Page 140
6.3.1 An Interpreter......Page 143
6.3.2 Assumptions Underlying the Implementation......Page 146
6.3.3 Correctness of the Interpreter for Basic Action Theories with Closed Initial Database......Page 147
6.3.4 The Elevator Example......Page 150
6.4 Discussion......Page 153
6.5 Proving Properties of Golog Programs......Page 155
6.5.1 Induction Principle for While Loops......Page 156
6.5.2 Example: A Blocks World......Page 157
6.6 Summary......Page 159
6.7 Exercises......Page 161
6.8 Bibliographic Remarks......Page 166
7.1 Concurrency and Instantaneous Actions......Page 170
7.2 Concurrency via Interleaving......Page 171
7.2.1 Examples of Interleaved Concurrency......Page 172
7.3 The Sequential, Temporal Situation Calculus......Page 173
7.3.1 Concurrent Temporal Processes......Page 175
7.4 Sequential, Temporal Golog......Page 176
7.4.1 Example: A Coffee Delivery Robot......Page 177
7.4.2 A Singing Robot......Page 183
7.4.3 Plan-Execution Monitoring......Page 184
7.5 The Concurrent, Non-Temporal Situation Calculus......Page 185
7.6.2 Action Precondition Axioms......Page 187
7.7 The Concurrent, Temporal Situation Calculus......Page 188
7.8 Concurrent, Temporal Golog......Page 190
7.9.1 Representing Physical Laws......Page 191
7.9.2 Permissiveness of the Situation Calculus......Page 192
7.9.3 Natural Actions and Executable Situations......Page 193
7.9.5 Zeno’s Paradox......Page 194
7.9.7 Least-Natural-Time Points......Page 195
7.9.8 Simulating Natural Worlds......Page 197
7.9.9 Animating Natural Worlds......Page 201
7.10 Exercises......Page 203
7.11 Bibliographic Remarks......Page 204
8.1 Interrupts......Page 206
8.2.1 Intuitive Semantics of RGolog......Page 208
8.2.2 Formal Semantics of RGolog......Page 209
8.3 An RGolog Interpreter......Page 211
8.4 Example: A Reactive Elevator Controller......Page 212
8.4.1 A Reactive Elevator with Interactively Generated Exogenous Actions......Page 214
8.4.2 A Reactive Elevator with Randomly Generated Exogenous Actions......Page 218
8.5 Interrupts with Priorities......Page 219
8.6 Discussion......Page 220
8.6.2 On-Line vs. Off-Line Program Execution......Page 221
8.7 Exercises......Page 223
8.8 Bibliographic Remarks......Page 224
9 Progression......Page 226
9.1 Logical Foundations of Progression......Page 228
9.1.1 Finite Progression Is Second-Order Definable......Page 230
9.2.1 Progressing Relatively Complete Databases......Page 231
9.2.2 Context-Free Successor State Axioms and the Progression of Isolated Fluents......Page 234
9.3.1 STRIPS Databases......Page 237
9.3.2 STRIPS Operator Descriptions......Page 239
9.3.3 Planning with STRIPS......Page 242
9.4 Strongly Context-Free Successor State Axioms......Page 244
9.5 Progression and Relational STRIPS......Page 245
9.6 An Open-World STRIPS......Page 247
9.7 Correctness of Relational and Open-World STRIPS......Page 249
9.8 Exercises......Page 251
9.9 Bibliographic Remarks......Page 252
10.1 A Simple Breadth-First Planner......Page 254
10.2 Example: Planning in the Blocks World......Page 256
10.2.1 A Planning Problem Example......Page 260
10.3 Planning with Concurrent Actions......Page 263
10.4 OCTOPUS: A Multi-Handed Blocks World Agent......Page 268
10.5 A Simple Depth-First Planner......Page 276
10.6.1 Prime Implicates and Compiling an Initial Database......Page 280
10.6.2 A Regression-Based Theorem-Prover......Page 287
10.6.4 Axiomatizing Incomplete Initial Situations......Page 289
10.6.5 A Blocks World with Incomplete Initial Situation......Page 291
10.7 Planning vs. Nondeterministic Programming......Page 296
10.8 Exercises......Page 298
10.9 Bibliographic Remarks......Page 301
11.1 Knowledge in the Situation Calculus......Page 304
11.1.1 Accessibility Relations and Knowledge......Page 305
11.1.2 Alternatives to the Initial Situation......Page 307
11.1.4 Knowledge and Action......Page 308
11.1.5 Knowledge Defined......Page 309
11.1.6 Some Consequences of This Approach......Page 310
11.1.7 A Useful Notation......Page 311
11.1.8 Quantifiers and Knowledge......Page 312
11.2 Knowledge and the Designer’s Perspective......Page 313
11.3 Knowledge-Producing Actions......Page 314
11.4.1 The No-Side-Effects Assumption for Knowledge-Producing Actions......Page 315
11.4.2 A Successor State Axiom for K......Page 316
11.4.4 Some Consequences of this Solution......Page 320
11.5.1 New Foundational Axioms for Situations......Page 323
11.5.2 Some Possible Accessibility Relations......Page 325
11.5.3 Basic Action Theories for Knowledge......Page 326
11.6 Regression for Knowledge-Producing Actions......Page 327
11.7 Knowledge-Based Programming......Page 330
11.7.2 Sense Actions......Page 333
11.7.3 Reducing Knowledge to Provability for the Initial Situation......Page 334
11.7.4 On-Line Execution of Knowledge-Based Programs......Page 335
11.7.5 Reduction of Knowledge to Provability for On-Line Programs......Page 336
11.7.6 The Dynamic Closed-World Assumption......Page 339
11.7.7 Interpreter for Knowledge-Based Programs with Sensing......Page 342
11.7.9 Putting It All Together......Page 343
11.8 Discussion......Page 348
11.9 Exercises......Page 349
11.10 Bibliographic Remarks......Page 353
12.1 Stochastic Actions and Probability......Page 356
12.1.1 How to Specify a Probabilistic Domain: A Guide for the Perplexed......Page 360
12.2 Derived Probabilities......Page 362
12.2.1 stGolog: Stochastic Golog......Page 366
12.3 Exogenous Events......Page 370
12.4 Uncertainty in the Initial Situation......Page 380
12.5 Markov Decision Processes......Page 384
12.5.1 Sensing and stGolog Programs......Page 387
12.5.2 Fully Observable MDPs......Page 390
12.5.3 Partially Observable MDPs......Page 393
12.5.4 Implementing Policies: Run-Time Sense Actions......Page 397
12.5.6 Solving MDP Planning Problems......Page 399
12.6 Discussion......Page 400
12.7 Exercises......Page 401
12.8 Bibliographic Remarks......Page 404
13 Concluding Remarks......Page 406
A.1 Decomposition Rules......Page 410
A.2 Generation Rules......Page 412
A.4 Proof Rules for Unique Names Axioms......Page 413
A.5 Simplification Rules......Page 414
A.7 Examples of Proofs......Page 415
A.8 Exercises......Page 420
B.1 Constraints and the Ramification Problem......Page 422
B.2 Constraints and the Qualification Problem......Page 423
B.3 Solving the Qualification and Ramification Problems......Page 425
Appendix C: Resources......Page 428
References......Page 430
D......Page 440
G......Page 441
M......Page 442
P......Page 443
S......Page 444
Z......Page 445