While mathematical software packages are commercially successful and widely used, the use of formal methods in hardware and software development is also becoming more and more important and necessary. This has made deduction systems indispensable because of the complexity and sheer size of the reasoning tasks involved. This volume is devoted to the

Manfred Kerber, Michael Kohlhase

Part I: Regular Contributions; Definite Integration of Parametric Rational Functions: Applying a DITLU; How to Find Symmetries Hidden in Combinatorial Problems; Communication Protocols for Mathematical Services based on KQML and OMRS; Interfacing Computer Algebra and Deduction Systems via the Logic Broker Architecture; Development of the Theory of Continuous Lattices in MIZAR; ?-ANTS - An Open Approach at Combining Interactive and Automated Theorem Proving; The TH?OREM? Project: A Progress Report; How to Formally and Efficiently Prove Prime(2999); On the EA-Style Integrated Processing of Self-Contained Mathematical Texts; Towards Learning New Methods in Proof Planning; Using Meta-variables for Natural Deduction in Theorema; Exploring Properties of Residue Classes; Defining Power Series and Polynomials in Mizar; Logic and Dependent Types in the Aldor Computer Algebra System; Part II: Invited Presentations; Communicating Mathematics on the Web; Teaching Mathematics Accross the Internet; Part III: System Description; Singular - A Computer Algebra System for Polynomial Computations; Part IV: Posters; Integration of Automated Reasoners: a Progress Report; Algorithmic Theories and Context; The GiNaC Framework for Symbolic Computation within the C++ Programming Language; A Framework for Propositional Model Elimination Algorithms; Resource Guided Concurrent Deduction; Automated 'Plugging and Chugging'; Integrating SAT Solvers with Domain-specific Reasoners; Solving Integrals at the Method Level; Lightweight Probability Theory for Verification; St Andrews CAAR Group: Poster Abstract; OpenXM - an Open System to Integrate Mathematical Software; Presentation of the Foc Project