J.UCS Special Issue on Integration of Deduction Systems

Abstract: Logic has become a cross-sectional formal specifcation language for applications in Artficial Intelligence, Computing, and Mathematics. Deduction is the corresponding derivation mechanism used to execute and analyse formal models, to predict properties, to generate plans or to detect errors. For about 35 years, researchers have developed different kinds of computational logics, calculi and computer programs for interactive and fully automated deduction.

In contemporary design of deduction systems there is a clearly observable trend away from monolithic systems towards building integrated tools. Thus the combinatorial power of fully automatic theorem provers might enhance the reasoning abilities of interactive specification and verification tools. Also, real world deduction problems tend to be so complex that no single methodology is likely to be successful. Though some high degree of maturity has been reached in various subfields of automated deduction, the obstacles to integration are still non-trivial and diverse. The aim of this special issue is to archive the state-of-the-art achieved in integration of deductive systems.

The idea for this special issue goes back to a workshop on 'Integration of Deduction Systems', held in conjunction with the International Conference on Automated Deduction 1998 (CADE), in Lindau, Germany. The large number of high quality submissions, and the very positive resonance to this largest satellite workshop of CADE 98 encouraged us to edit this special issue.

We received 13 submissions that underwent a careful review process. Based on 33 review reports we selected six regular papers, and two contributions that have the flavour of system descriptions. These are the papers Integrating Tps and Omega by C. Benzmüller, M. Bishop, and V. Sorge, and Interactive Verification Environments for Object-Oriented Programs by J. Meyer, and A. Poetzsch-Heffter.

The papers of this issue address the following integration topics:

• integration of first-order provers
  This is addressed in the paper Integrating Deduction Techniques in a Soft-ware Reuse Application by T. Baar, B. Fischer, and D. Fuchs.
• integration of higher-order provers
  See the paper Integrating Tps and Omega by C. Benzmüller, M. Bishop, and V. Sorge.
• combining first-order and higher-order provers
  This is tackled in Generic Tableau Prover and its Integration with Isabelle by L. C. Paulson.
• integration of calculi and logics
  This topic is dealt with in the papers Connection-based Theorem Proving in Classical and Non-classical Logics by Ch. Kreitz, J. Otten, and Proof Transformations from Search-oriented into Interaction-oriented Tableau Calculi by G. Stenz, W. Ahrendt, and B. Beckert.
• combining first-order logic and computer algebra
  This topic arises in the paper Loop-Detection in Hyper-Tableaux by Powerful Model Generation by F. Stolzenburg.
• integration of mathematical assistants
  This topic is addressed in the paper Agent-oriented Integration of Distributed Mathematical Services by A. Franke, S. M. Hess, Ch. G. Jung, M. Kohlhase, and V. Sorge.

We would like to thank all the authors for submitting their papers and all the reviewers for their valuable help in the selection process. Special thanks go to the Editor-in-Chief, Hermann Maurer, for hosting this special issue. We hope that all readers enjoy reading.