Automated deduction, CADE-19: 19th International Conference on Automated Deduction, Miami Beach, FL, USA, July 28-August 2, 2003 : proceedings

Cover
......Page 1
Automated Deduction –CADE-19: 19th International Conference on Automated Deduction, Miami Beach, FL, USA, July 28 – August 2, 2003, Proceedings
......Page 4
ISBN 3540405593......Page 5
Preface......Page 6
Program Committee......Page 8
Additional Reviewers......Page 9
Table of Contents......Page 10
SAT-Based Counterexample Guided Abstraction Refinement in Model Checking......Page 14
1 Introduction......Page 15
2 Prerequisites on Kripke Structures and LTL......Page 16
3 Simulations......Page 17
4 Rewriting Logic Specifications and Model Checking......Page 18
5 Equational Abstractions......Page 22
6 Related Work and Conclusions......Page 27
References......Page 28
1 Introduction......Page 30
2 Background......Page 32
3 Compatibility among Function Definitions......Page 34
4 Safe Generalizations by the No-Theory Condition......Page 39
5 A Decidable Class of Equational Conjectures......Page 41
6 Conclusion and Further Work......Page 43
References......Page 44
1 Introduction......Page 45
2 Dependency Pairs......Page 46
4 Cycle Analysis......Page 49
5 Argument Filterings......Page 52
6 Experiments......Page 56
References......Page 59
1 Introduction......Page 60
2 Preliminaries. Standard Knuth-Bendix Order......Page 61
3 The Ground Case......Page 64
4 Non-ground Order......Page 69
References......Page 71
1 Motivation......Page 73
2 Preliminaries......Page 75
3 Unary Coding of Numbers......Page 76
4 Binary Coding of Numbers......Page 80
5 ABox Consistency......Page 84
6 Outlook......Page 86
References......Page 87
1 Introduction......Page 103
2 Description Logics and Tableau Algorithms......Page 104
3 Alternating Automata......Page 106
4 Translating Alternating Automata into ELUf......Page 109
5 Two-Way Alternating Automata......Page 113
6 Implementation......Page 115
References......Page 116
1 Introduction......Page 119
2 The Safety Policy......Page 122
3 A Safety Proof......Page 128
4 Conclusion......Page 131
References......Page 132
1 Introduction......Page 134
2 Isabelle/HOL Notation......Page 135
3 A Simple Programming Language......Page 136
5 Lists on the Heap......Page 137
6 Inductive Data Types on the Heap......Page 140
7 The Schorr-Waite Algorithm......Page 141
References......Page 148
1 Introduction......Page 149
2 a......Page 152
3 ß......Page 156
4 Applications......Page 160
References......Page 162
1 Introduction......Page 164
2 Definition of PFsub......Page 165
3 Basic Proof Theory of PFsub......Page 171
4 Subtyping in PFsub......Page 172
5 Reduction to PF......Page 174
7 Conclusion......Page 176
References......Page 177
Reasoning about Quantiffiers by Matching in the E-graph......Page 179
1 Introduction......Page 180
3 The Algorithm for the Arithmetic Fragment......Page 182
4 Extension to Uninterpreted Function Symbols......Page 187
5 Retracting Assumptions......Page 189
6 Experimental Results......Page 191
7 Related Work......Page 192
References......Page 194
1 Introduction......Page 195
2 Preliminaries......Page 196
3 Basic Components......Page 197
4 Superposition......Page 205
References......Page 208
1 Introduction......Page 210
2 Preliminaries......Page 211
3 Combining Canonizers......Page 214
4 Convexity and Canonization......Page 218
5 Non-existence of Solvers......Page 221
6 Conclusion and Related Work......Page 222
References......Page 223
1 Introduction......Page 225
2 Definitions and Notations......Page 227
3 A Class of Equational Theories – TFE(S, R)......Page 228
4 Equational Proofs in TFE(S, R)......Page 229
5 Matching Problem in TFE(S, R)......Page 230
6 Unification Problem in TFE(S, R)......Page 232
7 Combination of Theories in TFE(S, R)......Page 234
8 Related Work......Page 237
9 Conclusion......Page 238
References......Page 239
1 Introduction......Page 241
3 Conditional Equations......Page 243
4 Vertical Sections, Lambda Calculus and Reification......Page 244
5 The Constructors iterate[x,y] and power[x]......Page 245
7 Arithmetic of Natural Numbers......Page 248
8 Laws of Exponents......Page 251
10 Schröder-Bernstein Theorem......Page 252
References......Page 253
1 Introduction......Page 256
2 Ordinals......Page 258
3 Definitions and Complexity......Page 261
4 Proofs of Correctness......Page 265
References......Page 269
1 Introduction......Page 272
2 Eight Queries Regarding Permutation Groups......Page 274
3 Formalisation Issues......Page 279
4 Proof Planning and Computer Algebra......Page 280
5 Planning the Subproblems......Page 282
6 Evaluation......Page 284
References......Page 286
1 Introduction......Page 288
2 Details of Implementation......Page 289
3 Current Advances......Page 291
References......Page 292
1 Introduction......Page 293
3 An Overview of IsaPlanner......Page 294
4 A Simple Induction Technique Encoded in IsaPlanner......Page 295
5 Some Results from Using the Induction Technique......Page 296
References......Page 297
1 Introduction......Page 303
2 User Interaction......Page 304
3 Improving the Quality of Conjectures......Page 305
5 Conclusions and Further Work......Page 306
Appendix A......Page 307
2 The Design of CASC-19......Page 309
3 Discussion......Page 310
1 Introduction......Page 311
2 Making Coq and ELAN Cooperating......Page 313
3 Construction of Proof Terms......Page 314
4 Proof Search and Proof Check for Equational Proofs......Page 316
5 Deduction Modulo and the Noetherian Induction Principle......Page 319
6 Proof Search and Proof Check for Inductive Proofs......Page 326
7 Conclusion......Page 327
References......Page 328
2 The WALDMEISTER Loop......Page 331
3 WALDMEISTER in Parallel......Page 333
References......Page 335
2 A Sketch of the Base Logic......Page 336
3 Working with  VeriFun......Page 338
References......Page 340
1 Why Another Inductive Theorem Prover?......Page 342
2 QuodLibet Specifications......Page 343
3 Proving Theorems with QuodLibet......Page 344
References......Page 346
Reasoning about Qualitative Representations of Space and Time......Page 348
1 Introduction......Page 349
2 A Motivating Example......Page 350
3 Language......Page 351
5 The Inference System......Page 353
6 Refutational Completeness......Page 356
8 Experiments......Page 361
References......Page 363
Translation of Resolution Proofs into Short First-Order Proofs without Choice Axioms......Page 379
1 Replacement of Function Symbols......Page 380
2 Translation of Resolution on the Clause Level......Page 383
3 Translation of the CNF-Transformation......Page 386
References......Page 392
1 Introduction......Page 426
2 The Idea of the Principle......Page 427
3 Translation to Clause Logic......Page 430
4 Incorporating Axioms into the Translation......Page 432
5 Completeness......Page 434
7 Other Consequences and Related Work......Page 437
8 Conclusions......Page 439
References......Page 440
1 Introduction......Page 441
2 Schematic Saturation......Page 443
3 Horn Clauses and Answer Substitutions......Page 449
4 Another Approach to Unification......Page 451
5 Conclusion......Page 454
References......Page 455
1 Introduction......Page 456
2 ACU I with Commuting Homomorphisms......Page 457
3 ACU IDl-Unification Is Decidable......Page 463
4 The ACU ID-Unification Problem......Page 467
References......Page 470
1 Introduction......Page 472
2 Motivating Example......Page 473
3 Notation and Basic Definitions......Page 475
4 Source-Tracking......Page 477
5 Unification Path Expressions......Page 478
6 Unification Algorithm with Source-Tracking......Page 479
7 Simplification of Unification Path Expressions......Page 481
8 Related Research......Page 483
9 Conclusions and Future Work......Page 484
References......Page 485
1 Introduction......Page 487
2 A Modal Foundation for Typed Existential Variables......Page 488
3 Toward Efficient Higher-Order Pattern Unification......Page 494
4 Experiments......Page 497
5 Related Work......Page 499
References......Page 500
1 Introduction......Page 502
2 Simply Typed Lambda Calculus......Page 504
3 Behavioral and Contextual Equivalences......Page 507
4 The Context Lemma......Page 508
5 A Computable Upper Bound for the Number of Equivalence Classes......Page 510
6 An Algorithm for Arity-Bounded and fv-Bounded HOMPs......Page 511
7 Remarks on the Complexity......Page 514
References......Page 515
Author Index......Page 517