Automated Deduction – CADE-20: 20th International Conference on Automated Deduction, Tallinn, Estonia, July 22-27, 2005. Proceedings

Cover
......Page 1
Automated Deduction –CADE-20: 20th International Conference on Automated Deduction, Tallinn, Estonia, July 22-27, 2005, Proceedings
......Page 3
ISBN-10 3540280057  ISBN-13 9783540280057......Page 4
Preface......Page 6
Program Committee......Page 8
External Reviewers......Page 9
Table of Contents......Page 12
1.2 A Proof-Search Method for the Theory H......Page 15
2.1 Resolution Modulo......Page 16
2.2 Proving Completeness......Page 17
3 From Consistency to Cut Elimination......Page 18
References......Page 20
1 Introduction......Page 37
2 TermsandPropositions......Page 39
3 Sequent Calculus......Page 40
4 Extensional Expansion Dags......Page 43
5 Search Operations......Page 46
6 Completeness of Search......Page 48
8 Conclusion......Page 50
References......Page 51
1 Introduction......Page 52
2 Preliminaries......Page 53
3 TheBijectiveSet......Page 54
4 Structural Induction Principle......Page 60
5 Examples......Page 62
6 Related Work......Page 65
7 Conclusion......Page 66
References......Page 67
1 Introduction......Page 68
2 Motivating Example: Sequent Calculus......Page 69
3 Tabling in Higher-Order Logic Programming......Page 72
3.1 Design of Memo-Table......Page 73
3.2 Optimization: Linearization......Page 74
3.3 Optimization: Strengthening......Page 75
4 Higher-Order Term Indexing for Tabling......Page 76
5 Compact Proof Witnesses......Page 77
6.1 Propositional Theorem Proving......Page 78
6.2 Refineent Type Checking......Page 79
7 Conclusion......Page 80
References......Page 81
1 Introduction......Page 98
2.1 Higher-Order Logic......Page 99
2.2 Uniform Notation......Page 100
2.3 Extensional Expansion Proofs......Page 102
3 CoReCalculus......Page 103
3.1 Admissible Replacement Rules......Page 104
4 Example......Page 109
5 Related Work and Conclusion......Page 111
References......Page 112
1 Introduction......Page 130
2.1 Weka and Classifier......Page 132
2.2 The Java Modeling Language......Page 133
3 A First Example: Joining Two Database Tables......Page 134
4 A Simple Data Privacy Preserving Classifie......Page 136
5 Privacy Through Non-interference......Page 137
5.2 Extension of Krakatoa......Page 138
6 Non-interference for the Naive Bayes Classifie......Page 139
7 Conclusion......Page 142
References......Page 143
1 Introduction......Page 163
2 Ellipsis Resolution......Page 164
3 Well-Nested Segments......Page 165
4 Context Unification......Page 166
5 Well-Nested Uniffiers......Page 168
6 Well-Nested Context Unification is in NP......Page 174
7 Conclusions......Page 176
References......Page 177
1 Introduction......Page 178
2 Preliminaries......Page 179
3 Termination-Preserving Transformations......Page 180
4 Termination......Page 182
4.1 Projecting Rewrite Derivations......Page 183
4.2 Lifting Rewrite Derivations......Page 185
4.3 Deciding Termination......Page 187
5 Conclusion......Page 189
References......Page 190
1 Introduction......Page 196
2 Temporal Models with Expanding Domains......Page 199
3 Recursive Enumerability......Page 202
4 Decidability......Page 205
5 Undecidable Problems for Channel Systems......Page 207
6 Non-recursive Enumerability......Page 208
7 Undecidability......Page 210
8 An Application to Dynamic Topological Logic......Page 214
9 Conclusion......Page 215
References......Page 216
1 Introduction......Page 218
2 First-Order Temporal Logic......Page 219
3 Monodic Temporal Resolution......Page 221
4 Decidability by Monodic Temporal Resolution......Page 223
5 Monodic Fine-Grained Temporal Resolution......Page 225
6 Decidability by Ordered Fine-Grained Resolution with Selection......Page 230
7 Future Work......Page 231
References......Page 232
1 Introduction......Page 233
1.1 Idea......Page 235
2 Basic Notions and Notations......Page 236
3 Embeddability......Page 238
4 Local Theory Extensions......Page 239
5.1 Flattening of Goals......Page 240
5.2 Embeddability of Weak Partial Models Implies Locality......Page 241
5.3 Embeddability of Evans Partial Models Implies Stable Locality......Page 242
6.1 Flattening and Relational Encoding......Page 243
6.2 Decidability and Complexity......Page 244
7 Beyond the Universal Fragment......Page 246
References......Page 247
1 Introduction......Page 249
2 Preliminaries......Page 250
3 Case-Study......Page 251
3.1 Properties......Page 253
4 Proof Planning for the Case-Study......Page 255
5 Experimental Results......Page 257
6 Conclusions, Related and Future Work......Page 260
References......Page 262
2 Proof Planning and Multi-Strategy Proof Planning......Page 264
3 TheMulti System......Page 265
4 Experiences and Case Studies......Page 267
References......Page 268
1 Introduction......Page 292
2 Notation and Definitions......Page 294
3 Positive Algebraic Completions and Compatibility......Page 297
4 The Main Combination Result......Page 299
5 A Variant of the Connection Scheme......Page 303
7 Conclusion......Page 306
References......Page 307
1 Introduction......Page 336
2 Background......Page 337
3.1 The Need for XOR Constraints......Page 339
3.2 Deduction with XOR Constraints......Page 341
3.4 Simplification with XOR Constraints......Page 342
4.1 The 4758 CCA Attacks......Page 343
4.2 Attacking a Variant of the Needham–Schroeder–Lowe Protocol......Page 345
5 Conclusions......Page 346
References......Page 349
ACU Automata......Page 359
XOR and AG......Page 361
3 and Two-Way Automata......Page 363
1 Introduction......Page 367
2.1 Theory-Speci.c Interpolants......Page 369
3 The Combination Method......Page 371
3.1 Partial Interpolants......Page 374
4 Equality-Interpolating Theories......Page 376
5 Interpolants for Arbitrary Quantiffier-Free Formulas......Page 378
6 Related Work......Page 380
7 Conclusions and Future Work......Page 381
References......Page 382
1 Introduction......Page 391
2 Preliminaries......Page 393
3 Attacks with Regular Knowledge......Page 395
3.1 Stage Theories......Page 396
3.2 DAG of the Attack......Page 397
4 Protocols with Regular Constraints......Page 400
5 Regular Protocols......Page 401
6 Conclusions......Page 404
References......Page 405
1 Introduction......Page 423
2 Basic Concepts of Model Representation......Page 424
2.1 Contexts and Model Evolution......Page 425
2.2 Explicit and Implicit Generalizations......Page 427
3 Expressive Power of DIGs and Contexts......Page 429
4 Clause Evaluation and Testing Equivalence......Page 431
5 Related Work......Page 434
6 Conclusion......Page 435
References......Page 436
1 Introduction......Page 438
2 MerkleTree......Page 439
3.1 (W )S2S......Page 441
3.2 MONA......Page 442
4.1 Incremental Merkle Forest
......Page 443
4.2 Incremental Scheme for Optimal Slice Replication......Page 445
5 Characterization as a Pivoted Forest......Page 446
6.2 Proving Theorem 1 by Induction......Page 449
6.3 Proving Theorem 1 by MONA......Page 450
7.2 Proving Weak Consistency......Page 451
7.3 Proving Consistency......Page 452
8 Conclusion......Page 453
References......Page 454
1 Introduction......Page 455
2 Search Programs......Page 456
3 Useful Mathematical Results......Page 457
4.1 Size 7 by FALCON......Page 459
5.2 The Case of Size 9......Page 460
6 Some Experiences......Page 461
Acknowledgements......Page 463
Appendix......Page 464
1.1 The Need for Mobile Reasoning......Page 466
2.2 Description Logics Transformation......Page 467
3.1 Using the First Order Reasoner......Page 469
4.1 Conclusions......Page 470
References......Page 471
Author Index......Page 473