Automated Reasoning: Second International Joint Conference, IJCAR 2004, Cork, Ireland, July 4-8, 2004. Proceedings

José Meseguer, Grigore Roşu (auth.), David Basin, Michaël Rusinowitch (eds.)3-540-25984-8, 3-540-22345-2

This volume constitutes the proceedings of the 2nd International Joint C- ference on Automated Reasoning (IJCAR 2004) held July 4–8, 2004 in Cork, Ireland. IJCAR 2004 continued the tradition established at the ?rst IJCAR in Siena,Italyin2001,whichbroughttogetherdi?erentresearchcommunitieswo- ing in automated reasoning. The current IJCAR is the fusion of the following conferences: CADE: The International Conference on Automated Deduction, CALCULEMUS: Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, FroCoS: Workshop on Frontiers of Combining Systems, FTP: The International Workshop on First-Order Theorem Proving, and TABLEAUX: The International Conference on Automated Reasoning with Analytic Tableaux and Related Methods. There were 74 research papers submitted to IJCAR as well as 12 system descriptions. After extensive reviewing, 26 research papers and 6 system – scriptions were accepted for presentation at the conference and publication in this volume. In addition, this volume also contains papers from the three invited speakers and a description of the CADE ATP system competition. We would like to acknowledge the enormous amount of work put in by the members of the program committee, the various organizing and steering c- mittees, the IJCAR o?cials, the invited speakers, and the additional referees named on the following pages. We would also like to thank Achim Brucker and Barbara Geiser for their help in producing this volume.

---

Table of contents :
Front Matter….Pages –
Rewriting Logic Semantics: From Language Specifications to Formal Analysis Tools….Pages 1-44
A Redundancy Criterion Based on Ground Reducibility by Ordered Rewriting….Pages 45-59
Efficient Checking of Term Ordering Constraints….Pages 60-74
Improved Modular Termination Proofs Using Dependency Pairs….Pages 75-90
Deciding Fundamental Properties of Right-(Ground or Variable) Rewrite Systems by Rewrite Closure….Pages 91-106
Redundancy Notions for Paramodulation with Non-monotonic Orderings….Pages 107-121
A Resolution Decision Procedure for the Guarded Fragment with Transitive Guards….Pages 122-136
Attacking a Protocol for Group Key Agreement by Refuting Incorrect Inductive Conjectures….Pages 137-151
Decision Procedures for Recursive Data Structures with Integer Constraints….Pages 152-167
Modular Proof Systems for Partial Functions with Weak Equality….Pages 168-182
A New Combination Procedure for the Word Problem That Generalizes Fusion Decidability Results in Modal Logics….Pages 183-197
Using Automated Theorem Provers to Certify Auto-generated Aerospace Software….Pages 198-212
argo-lib : A Generic Platform for Decision Procedures….Pages 213-217
The ICS Decision Procedures for Embedded Deduction….Pages 218-222
System Description: E 0.81….Pages 223-228
Second-Order Logic over Finite Structures – Report on a Research Programme….Pages 229-243
Efficient Algorithms for Constraint Description Problems over Finite Totally Ordered Domains….Pages 244-258
PDL with Negation of Atomic Programs….Pages 259-273
Counter-Model Search in Gödel-Dummett Logics….Pages 274-288
Generalised Handling of Variables in Disconnection Tableaux….Pages 289-306
Chain Resolution for the Semantic Web….Pages 307-320
Sonic — Non-standard Inferences Go OilEd ….Pages 321-325
TeMP : A Temporal Monodic Prover….Pages 326-330
Dr.Doodle: A Diagrammatic Theorem Prover….Pages 331-335
Solving Constraints by Elimination Methods….Pages 336-341
Analyzing Selected Quantified Integer Programs….Pages 342-356
Formalizing O Notation in Isabelle/HOL….Pages 357-371
Experiments on Supporting Interactive Proof Using Resolution….Pages 372-384
A Machine-Checked Formalization of the Generic Model and the Random Oracle Model….Pages 385-399
Automatic Generation of Classification Theorems for Finite Algebras….Pages 400-414
Efficient Algorithms for Computing Modulo Permutation Theories….Pages 415-429
Overlapping Leaf Permutative Equations….Pages 430-444
TaMeD: A Tableau Method for Deduction Modulo….Pages 445-459
Lambda Logic….Pages 460-474
Formalizing Undefinedness Arising in Calculus….Pages 475-489
The CADE ATP System Competition….Pages 490-491
Back Matter….Pages –