Preface v Table of Contents ix List of Contributors xi Programming in Alma-O, or Imperative and Declarative Programming Reconciled 1(16) Krzysztof R. Apt Andrea Schaerf Church-Rosser Property for Conditional Rewriting Systems with Built-in Predicates as Premises 17(22) Mauricio Ayala-Rincon Combining WS1S and HOL 39(18) David Basin Stefan Friedrich A Recipe for the Complexity Analysis of Non-Classical Logics 57(20) David Basin Luca Vigano Computer Arithmetic: Logic, Calculation and Rewriting 77(18) Marco Benini Dirk Nowotka Carl Pulley Combining Higher-Order and First-Order Computation Using ρ-Calculus: Towards a Semantics of ELAN 95(26) Horatiu Cirstea Claude Kirchner Distributed First Order Logic 121(20) Chiara Ghidini Luciano Serafini Pushing the Frontiers of Combining Rewrite Systems Farther Outwards 141(20) Jurgen Giesl Enno Ohlebusch Toward Sharing Libraries of Mathematics between Theorem Provers 161(16) Douglas J. Howe Negation in Combining Constraint Systems 177(16) Stephan Kepser Optimisation Techniques for Combining Constraint Solvers 193(18) Stephan Kepser Jorn Richts The Constraint Solver Collaboration Language of BALI 211(20) Eric Monfroy A Hybrid Language for the Analysis of Aspectual and Temporal Phenomena in Natural Language 231(24) Ralf Naumann Combining Semantical and Syntactical Theory Reasoning 255(20) Uwe Petermann A Generic Approach to Combining Stochastic Algorithms with Systematic Constraint Solvers 275(20) Steven Prestwich Categorial Fibring of Logics with Terms and Binding Operators 295(22) Amilcar Sernadas Cristina Sernadas Carlos Caleiro Till Mossakowski Iterative Dialogue and Automated Proofs 317(20) Konrad Slind Richard Boulton Towards Heterogeneous Specifications 337(24) Andrzej Tarlecki Integration of Linear Arithmetic and Goal-Oriented Resolution for Software Reasoning 361(18) Tie-Chung Wang Allen Goldberg Temporalizing Description Logics 379(24) Frank Wolter Michael Zakharyaschev Index 403