Automated Deduction — CADE-16: 16th International Conference on Automated Deduction Trento, Italy, July 7–10, 1999 Proceedings

Cover
......Page 1
Automated Deduction – CADE-16: 16th International Conference on Automated Deduction, Trento, Italy, July 7-10, 1999, Proceedings......Page 4
ISBN 3540662227......Page 5
Preface......Page 6
Conference Organization......Page 7
Table of Contents......Page 10
1 Introduction......Page 14
2 The Lambek Calculus......Page 15
3 Proof-nets for the Lambek calculus......Page 16
4 Grammars of axiom links......Page 20
5 The proof-net construction algorithm......Page 25
6 Conclusions and future work......Page 27
A Chomsky normal form of System R3......Page 28
1 Introduction......Page 29
2 Provability Logics......Page 30
3 Display Calculi......Page 32
4 Transformations from LF into L......Page 36
5 Another Characterisation......Page 40
References......Page 41
1 Introduction......Page 44
2 Guarded Logics......Page 47
3 Guarded Bisimulation and the Tree Model Property......Page 51
4 Decision Procedures......Page 53
References......Page 64
1 Introduction......Page 65
2 Preliminaries......Page 66
3 Reasoning for Gr(K )......Page 67
4 An Optimal Solution......Page 72
5 Conclusion......Page 77
References......Page 79
1 Introduction......Page 80
2 Formal Preliminaries......Page 82
3 Generalized Context Problems......Page 84
4 Translation into Generalized Context Problems......Page 86
5 Translation of Generalized Context Problems into Word Equations with Regular Constraints......Page 87
6 Identification of Letter Descriptions......Page 89
References......Page 93
1 Introduction......Page 95
2 Definitions and Basic Facts......Page 97
3 Coding SAT Problems in Higher Order Matching......Page 101
4 Fourth Order Matching is NEXPTIME-Hard......Page 105
5 Final Remarks......Page 107
References......Page 108
1 Introduction......Page 110
2 Preliminaries......Page 111
3 Main Sources of Complexity......Page 113
4 Parameter-Free Equations......Page 115
5 NP-Membership......Page 120
6 Conclusions and Future Work......Page 122
References......Page 124
1 Introduction......Page 125
2 Symbolic Definite Integration......Page 126
3 The VSDITLU......Page 131
4 Our Implementation......Page 136
5 Discussion......Page 137
References......Page 138
1 Introduction......Page 140
2 Background and Notation......Page 142
3 Heaviest Non-T -Term......Page 143
4 Simplification Procedures......Page 145
5 Extended Proof Method......Page 147
6 Worked Example
......Page 148
7 Properties of Extended Proof Method......Page 149
8 Implementation and Results......Page 150
10 Related Work......Page 152
References......Page 153
1 Introduction......Page 170
2 Preliminaries......Page 171
3 On the Universal Theory of Subvarieties of DLO......Page 174
4 Experiments......Page 182
References......Page 183
1 Introduction......Page 185
2 The Class K and Quasi-regular Clauses......Page 186
3 Resolution and Factoring on Quasi-regular Clauses......Page 188
4 An Atom Ordering for Quasi-regular Clauses......Page 189
5 A Decision Procedure for KC......Page 194
6 An Extension of KC: The Class DKC......Page 196
7 Conclusion......Page 198
References......Page 199
1 Introduction......Page 200
2 Basic Issues in Description Logic......Page 201
3 Decision Methods for Description Logics......Page 204
4 Extensions and Variations......Page 211
5 Related Work......Page 212
6 Conclusions and Further Work......Page 213
References......Page 214
1 The Twelf System......Page 215
2 Implementation......Page 217
3 Environment......Page 218
References......Page 219
2 System Description......Page 220
References......Page 223
1 Introduction......Page 225
3 Intended Extensions......Page 227
References......Page 229
2 Implementation......Page 230
3 Existing Mathematical Services......Page 231
4 Applications and Experiences......Page 232
References......Page 233
1 Skolem Verification Conditions......Page 235
2 An OBDD-Based Deductive Selection Method......Page 236
3 Example: Szymanski\'s Algorithm......Page 237
References......Page 239
2 Related Work......Page 240
4 Distributed Refinement......Page 241
5 Performance Measurements......Page 243
References......Page 244
2 Enlarging the Hypothesis......Page 245
3 Controlling the Proof Search......Page 246
References......Page 249
1 Introduction......Page 250
2 Example......Page 252
3 Protocol Verification in Nuprl......Page 253
4 Overview of Data Abstraction......Page 255
5 Defining Representability in Nuprl......Page 257
6 Main Results of the Nuprl Formalization......Page 259
7 Some Details of the Nuprl Proofs......Page 261
8 Conclusion......Page 263
References......Page 264
1 Introduction......Page 265
System......Page 268
4 Program Analysis......Page 274
5 Conclusion......Page 277
References......Page 278
1 Introduction......Page 280
2 Verification Systems......Page 282
3 Stability Equals Admissibility of Reflection Rule......Page 283
4 Provability Tests and Other Sources of Reflection......Page 285
5 Metamathematical Cost of Soundness and Stability......Page 286
6 Metamathematical Cost of Implicit Reflection......Page 289
7 Explicit Reflection for Verification Systems......Page 290
8 Practical Suggestions......Page 292
References......Page 293
2 Theoretical Background......Page 295
3 Building Constraint Tableaux......Page 296
4 Solving Constraints in Oz......Page 297
5 System Performance......Page 298
References......Page 299
System Description: Teyjus|A Compiler and Abstract Machine Based Implementation of Prolog......Page 300
References......Page 303
2 Compiling and Indexing......Page 305
3 Other Features......Page 306
5 Performance......Page 307
References......Page 309
2 Calculus......Page 310
3 Search Control......Page 311
4 Implementation......Page 312
5 Experimental Results......Page 313
References......Page 314
1 Introduction......Page 315
2 Ordered Paramodulation, Redundancy, and Saturation......Page 316
3 Perspectives......Page 318
References......Page 324
1 Introduction......Page 327
2 The Neuman{Stubblebine Protocol......Page 328
3 Monadic Horn Theories......Page 334
4 Conclusion......Page 340
References......Page 341
1 Introduction......Page 342
2 A Confluent Connection Calculus......Page 346
3 Completeness......Page 352
4 Conclusions......Page 354
References......Page 355
1 Introduction......Page 357
2 Connection Tableau Calculus......Page 358
3 Relevancy-Based Clause Selection with Abstractions......Page 361
4 Case Study: Symbol Abstractions......Page 366
5 Experiments with Lemma Selection......Page 369
References......Page 371
1 Introduction......Page 372
2 Component Search......Page 374
3 Unification......Page 379
5 Results......Page 382
6 Conclusions and Further Work......Page 384
References......Page 385
1 Introduction......Page 387
2 Problem Selection and System Evaluation......Page 388
3 Problem Presentation......Page 389
References......Page 390
2 New Features......Page 391
References......Page 395
3 The Tableau Method Implementation......Page 396
4 The Inverse Method Implementation......Page 397
5 Experiments......Page 398
6 Further Developments......Page 399
References......Page 400
System Description: CYNTHIA......Page 401
1 An Example of Using C NTHIA......Page 402
2 Representing ML De nitions as Proofs......Page 403
References......Page 405
2 The Approach......Page 406
3 Experiments......Page 408
4 Concluding Remarks......Page 409
References......Page 410
References......Page 411
1 Introduction......Page 412
2 Higher-Order (HO) Logic......Page 413
3 ER: Extensional HO Resolution......Page 416
5 EP : Extensional HO Paramodulation......Page 418
6 ERUE : Extensional HO RUE-Resolution......Page 423
7 Examples......Page 424
8 Conclusion......Page 425
References......Page 426
1 Introduction......Page 427
2 Outline of the Methodology......Page 428
3 Second-Order Logic......Page 429
4 TheP2 Algorithm......Page 431
5 Experiments with P2......Page 436
6 Properties of the Generated Provers......Page 439
7 Conclusions and Related Work......Page 440
References......Page 441
Author Index......Page 442