J.UCS Special Issue on Integration of Deduction Systems
R. Hähnle, W. Menzel, P.H. Schmitt
(University of Karlsruhe, Germany
(University of Ulm, Germany
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
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.
Wolfgang Reif, Guest Editor
Universität Ulm, D-89069 Ulm,
Reiner Hähnle, Wolfram Menzel, Peter H. Schmitt, Guest
Institut für Logik, Komplexität
Universität Karlsruhe, D-76128 Karlsruhe,