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.
Author(s): Ian Horrocks (auth.), Andrei Voronkov (eds.)
Series: Lecture Notes in Computer Science 2392 : Lecture Notes in Artificial Intelligence
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 2002
Language: English
Pages: 540
Tags: Artificial Intelligence (incl. Robotics); Mathematical Logic and Formal Languages; Logics and Meanings of Programs; Programming Languages, Compilers, Interpreters
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
