Automated deduction--CADE 16: 16th International; Conference on Automated Deduction, Trento, Italy, July 7-10, 1999 : proceedings

This book constitutes the refereed proceedings of the 16th International Conference on Automated Deduction, CADE-16, held in Trento, Italy in July 1999 as part of FLoC'99. The 21 revised full papers presented were carefully reviewed and selected from a total of 83 submissions. Also included are 15 system descriptions and two invited full papers. The book addresses all current issues in automated deduction and theorem proving, ranging from logical foundations to deduction systems design and evaluation 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 This volume constitutes the refereed proceedings of the 16th International Conference on Automated Deduction held in Italy in July 1999. It addresses recent issues in automated deduction and theorem proving, ranging from logical foundations to deduction systems design and evaluation.