Automated Deduction - CADE-18: 18th International Conference on Automated Deduction, Copenhagen, Denmark, July 27-30, 2002 Proceedings (Lecture Notes in Computer Science, 2392)

The First CADE in the Third Millennium This volume contains the papers presented at the Eighteenth International C- ference on Automated Deduction (CADE-18) held on July 27–30th, 2002, at the University of Copenhagen as part of the Federated Logic Conference (FLoC 2002). Despite a large number of deduction-related conferences springing into existence at the end of the last millennium, the CADE conferences continue to be the major forum for the presentation of new research in all aspects of automated deduction. CADE-18 was sponsored by the Association for Auto- ted Reasoning, CADE Inc., the Department of Computer Science at Chalmers University, the Gesellschaft fur ̈ Informatik, Safelogic AB, and the University of Koblenz-Landau. There were 70 submissions, including 60 regular papers and 10 system - scriptions. Each submission was reviewed by at least ?ve program committee members and an electronic program committee meeting was held via the Int- net. The committee decided to accept 27 regular papers and 9 system descr- tions. One paper switched its category after refereeing, thus the total number of system descriptions in this volume is 10. In addition to the refereed papers, this volume contains an extended abstract of the CADE invited talk by Ian Horrocks, the joint CADE/CAV invited talk by Sharad Malik, and the joint CADE-TABLEAUX invited talk by Matthias Baaz. One more invited lecture was given by Daniel Jackson. Reasoning with Expressive Description Logics: Theory and Practice....Pages 1-15 Temporal Logic for Proof-Carrying Code....Pages 16-30 A Gradual Approach to a More Trustworthy, Yet Scalable, Proof-Carrying Code....Pages 31-46 Formal Verification of a Java Compiler in Isabelle....Pages 47-62 Embedding Lax Logic into Intuitionistic Logic....Pages 63-77 Combining Proof-Search and Counter-Model Construction for Deciding Gödel-Dummett Logic....Pages 78-93 Connection-Based Proof Search in Propositional BI Logic....Pages 94-110 DDDLIB: A Library for Solving Quantified Difference Inequalities....Pages 111-128 An LCF-Style Interface between HOL and First-Order Logic....Pages 129-133 System Description: The MathWeb Software Bus for Distributed Mathematical Reasoning....Pages 134-138 Proof Development with Ω mega ....Pages 139-143 LearnΩmatic: System Description....Pages 144-149 HyLoRes 1.0: Direct Resolution for Hybrid Logics....Pages 150-155 Testing Satisfiability of CNF Formulas by Computing a Stable Set of Points....Pages 156-160 A Note on Symmetry Heuristics in SEM....Pages 161-180 A SAT Based Approach for Solving Formulas over Boolean and Linear Mathematical Propositions....Pages 181-194 Deductive Search for Errors in Free Data Type Specifications Using Model Generation....Pages 195-210 Reasoning by Symmetry and Function Ordering in Finite Model Generation....Pages 211-225 Algorithmic Aspects of Herbrand Models Represented by Ground Atoms with Ground Equations....Pages 226-240 A New Clausal Class Decidable by Hyperresolution....Pages 241-259 Spass Version 2.0....Pages 260-274 System Description: GrAnDe 1.0....Pages 275-279 The HR Program for Theorem Generation....Pages 280-284 AutoBayes/CC — Combining Program Synthesis with Automatic Code Certification — System Description —....Pages 285-289 The Quest for Efficient Boolean Satisfiability Solvers....Pages 290-294 Recursive Path Orderings Can Be Context-Sensitive....Pages 295-313 Shostak Light....Pages 314-331 Formal Verification of a Combination Decision Procedure....Pages 332-346 Combining Multisets with Integers....Pages 347-362 The Reflection Theorem: A Study in Meta-theoretic Reasoning....Pages 363-376 Faster Proof Checking in the Edinburgh Logical Framework....Pages 377-391 Solving for Set Variables in Higher-Order Theorem Proving....Pages 392-407 The Complexity of the Graded μ -Calculus....Pages 408-422 Lazy Theorem Proving for Bounded Model Checking over Infinite Domains....Pages 423-437 Well-Foundedness Is Sufficient for Completeness of Ordered Paramodulation....Pages 438-455 Basic Syntactic Mutation....Pages 456-470 The Next Waldmeister Loop....Pages 471-485 Focussing Proof-Net Construction as a Middleware Paradigm....Pages 486-500 Proof Analysis by Resolution....Pages 501-516 ....Pages 517-531 This book constitutes the refereed proceedings of the 18th International Conference on Automated Deduction, CADE - 18, held in Copenhagen, Denmark, in July 2002. The 27 revised full papers and 10 system descriptions presented together with three invited contributions were carefully reviewed and selected from 70 submissions. The book offers topical sections on description logics and the semantic Web, proofcarrying code and compiler verifications, non-classical logics, system descriptions, SAT, model generation, CASC, combination and decision procedures, logical frameworks, model checking, equational reasoning, and proof theory